Difference between revisions of "Json"
Jump to navigation
Jump to search
m (→Examples) |
m |
||
(One intermediate revision by the same user not shown) | |||
Line 1: | Line 1: | ||
− | In [[Mini Micro]], <c>json</c> is an [[import]] module in the <c>/sys/lib</c> directory. It provides conversion of MiniScript values to and from JSON format, as well as some related utility functions. | + | In [[Mini Micro]], <c>json</c> is an [[import]] module in the <c>/sys/lib</c> directory. It provides conversion of MiniScript values to and from [https://www.json.org/ JSON] format, as well as some related utility functions. |
− | + | Like all the modules in <c>/sys/lib</c>, the best documentation for the json module is the source code (<c>/sys/lib/json.ms</c>) itself. But this page summarizes the content in more concise form. | |
− | |||
− | Like all the modules in <c>/sys/lib</c>, the best documentation for | ||
== Functions == | == Functions == |
Latest revision as of 17:41, 12 September 2021
In Mini Micro, json
is an import module in the /sys/lib
directory. It provides conversion of MiniScript values to and from JSON format, as well as some related utility functions.
Like all the modules in /sys/lib
, the best documentation for the json module is the source code (/sys/lib/json.ms
) itself. But this page summarizes the content in more concise form.
Functions
After importing "json", the following methods may be accessed under the json
map (e.g. as json.parse
).
Method | Purpose |
---|---|
parse(jsonString) | parses JSON data into native MiniScript values |
toJSON(value, compact=false, indent=0) | converts MiniScript values into JSON format |
hexToInt(s) | convert hexadecimal string (e.g. "002A") to the equivalent number (42) |
escape(s) | change special characters into backslash sequences |
unescape(s) | replace backslash sequences with normal characters |
Examples
The following example builds a simple MiniScript data structure, then writes this out to a file in JSON format.
import "json"
data = {"name":"Alice", "job":"Engineer"}
data.kids = []
data.kids.push {"name":"Billy", "age":8}
data.kids.push {"name":"Mary", "age":12}
f = file.open("data.json")
f.write json.toJSON(data)
f.close
The example below reads and parses the JSON file created above, then prints out the age of the first child.
import "json"
data = json.parse(file.open("data.json").read)
print data.kids[0].age