diff --git a/src/org/rascalmpl/library/lang/json/IO.rsc b/src/org/rascalmpl/library/lang/json/IO.rsc index 3c8a9f3dede..463c8f299c4 100644 --- a/src/org/rascalmpl/library/lang/json/IO.rsc +++ b/src/org/rascalmpl/library/lang/json/IO.rsc @@ -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} diff --git a/src/org/rascalmpl/library/util/Benchmark.rsc b/src/org/rascalmpl/library/util/Benchmark.rsc index 6e89b030c76..eb6405b0dac 100644 --- a/src/org/rascalmpl/library/util/Benchmark.rsc +++ b/src/org/rascalmpl/library/util/Benchmark.rsc @@ -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)}