2017-06-25 17:51:08 +02:00
|
|
|
// JSON (http://www.json.org)
|
2017-07-29 20:04:22 +02:00
|
|
|
ws:alias = [ \b\f\n\r\t];
|
2017-06-25 17:51:08 +02:00
|
|
|
true = "true";
|
|
|
|
false = "false";
|
|
|
|
null = "null";
|
2017-07-29 20:04:22 +02:00
|
|
|
string = "\"" ([^\\"\b\f\n\r\t] | "\\" (["\\/bfnrt] | "u" [0-9a-f]{4}))* "\"";
|
|
|
|
number = "-"? ("0" | [1-9][0-9]*) ("." [0-9]+)? ([eE] [+\-]? [0-9]+)?;
|
|
|
|
entry = string ws* ":" ws* value;
|
|
|
|
object = "{" ws* (entry ws* ("," ws* entry)*)? ws* "}";
|
|
|
|
array = "[" ws* (value ws* ("," ws* value)*)? ws* "]";
|
2017-06-25 17:51:08 +02:00
|
|
|
value:alias = true | false | null | string | number | object | array;
|
2017-07-30 05:55:04 +02:00
|
|
|
json:root = ws* value ws*;
|