Skip to content

Commit

Permalink
Merge pull request #1922 from linuswagner/main
Browse files Browse the repository at this point in the history
Document some parameters for JSON.writeJSON
  • Loading branch information
jurgenvinju authored Mar 9, 2024
2 parents 51400dd + a646235 commit 6e61534
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 0 deletions.
5 changes: 5 additions & 0 deletions src/org/rascalmpl/library/lang/json/IO.rsc
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,11 @@ In general the translation behaves as the same as for ((readJSON)).}
java &T parseJSON(type[&T] expected, str src, str dateTimeFormat = "yyyy-MM-dd\'T\'HH:mm:ssZZZZZ", bool lenient=false, bool trackOrigins=false);

@javaClass{org.rascalmpl.library.lang.json.IO}
@synopsis{writes `val` to the location `target`}
@description{
If `dateTimeAsInt` is set to `true`, the dateTime values are converted to an int that represents the number of milliseconds from 1970-01-01T00:00Z.
If `indent` is set to a number greater than 0, the JSON file will be formatted with `indent` number of spaces as indentation.
}
java void writeJSON(loc target, value val, bool unpackedLocations=false, str dateTimeFormat="yyyy-MM-dd\'T\'HH:mm:ssZZZZZ", bool dateTimeAsInt=false, int indent=0, bool dropOrigins=true);

@javaClass{org.rascalmpl.library.lang.json.IO}
Expand Down
3 changes: 3 additions & 0 deletions src/org/rascalmpl/library/util/Benchmark.rsc
Original file line number Diff line number Diff line change
Expand Up @@ -44,13 +44,16 @@ The number can change over time but it's never higher than ((getMaxMemory))`
java int getTotalMemory();

@synopsis{Returns the maximum amount of memory that is available to the current JVM}
@description{Amount returned in bytes.}
@javaClass{org.rascalmpl.library.util.Benchmark}
java int getMaxMemory();

@synopsis{Returns the amount of memory that is currently in use by the programs running on this JVM}
@description{Amount returned in bytes.}
int getUsedMemory() = getTotalMemory() - getFreeMemory();

@synopsis{Returns the amount of memory that is yet available, in principle, on the current JVM}
@description{Amount returned in bytes.}
int getMaxFreeMemory() = getMaxMemory() - getUsedMemory();

@synopsis{CPU time in nanoseconds (10^-9^ sec)}
Expand Down

0 comments on commit 6e61534

Please sign in to comment.