Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Document some parameters for JSON.writeJSON #1922

Merged
merged 2 commits into from
Mar 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading