author | wenzelm |
Sun, 11 Mar 2018 15:06:48 +0100 | |
changeset 67819 | b73d8ed73b35 |
parent 67736 | 65016740d3e0 |
child 67841 | 8ada8f6d9495 |
permissions | -rw-r--r-- |
63992 | 1 |
/* Title: Pure/General/json.scala |
63644 | 2 |
Author: Makarius |
3 |
||
67819 | 4 |
Support for JSON: https://www.json.org/. |
63644 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
10 |
import scala.util.parsing.combinator.Parsers |
66922 | 11 |
import scala.util.parsing.combinator.lexical.Scanners |
12 |
import scala.util.parsing.input.CharArrayReader.EofCh |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
13 |
|
66922 | 14 |
|
63644 | 15 |
object JSON |
16 |
{ |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
17 |
type T = Any |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
18 |
type S = String |
63644 | 19 |
|
66928 | 20 |
type Object = Map[String, T] |
21 |
val empty: Object = Map.empty |
|
22 |
||
63644 | 23 |
|
66922 | 24 |
/* lexer */ |
25 |
||
26 |
object Kind extends Enumeration |
|
27 |
{ |
|
28 |
val KEYWORD, STRING, NUMBER, ERROR = Value |
|
29 |
} |
|
30 |
||
31 |
sealed case class Token(kind: Kind.Value, text: String) |
|
32 |
{ |
|
33 |
def is_keyword: Boolean = kind == Kind.KEYWORD |
|
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
34 |
def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name |
66922 | 35 |
def is_string: Boolean = kind == Kind.STRING |
36 |
def is_number: Boolean = kind == Kind.NUMBER |
|
37 |
def is_error: Boolean = kind == Kind.ERROR |
|
38 |
} |
|
39 |
||
40 |
object Lexer extends Scanners with Scan.Parsers |
|
41 |
{ |
|
42 |
override type Elem = Char |
|
43 |
type Token = JSON.Token |
|
44 |
||
45 |
def errorToken(msg: String): Token = Token(Kind.ERROR, msg) |
|
46 |
||
67111
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
47 |
val white_space: String = " \t\n\r" |
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
48 |
override val whiteSpace = ("[" + white_space + "]+").r |
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
49 |
def whitespace: Parser[Any] = many(character(white_space.contains(_))) |
66922 | 50 |
|
51 |
val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_))) |
|
52 |
val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_))) |
|
53 |
||
54 |
def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_))) |
|
55 |
def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_))) |
|
56 |
||
57 |
||
58 |
/* keyword */ |
|
59 |
||
60 |
def keyword: Parser[Token] = |
|
66924 | 61 |
(letters1 | one(character("{}[],:".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s)) |
66922 | 62 |
|
63 |
||
64 |
/* string */ |
|
65 |
||
66 |
def string: Parser[Token] = |
|
67 |
'\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) |
|
68 |
||
69 |
def string_body: Parser[Char] = |
|
67111
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
70 |
elem("", c => c > '\u001f' && c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape |
66922 | 71 |
|
72 |
def string_escape: Parser[Char] = |
|
73 |
elem("", "\"\\/".contains(_)) | |
|
74 |
elem("", "bfnrt".contains(_)) ^^ |
|
75 |
{ case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | |
|
76 |
'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ |
|
77 |
(s => Integer.parseInt(s, 16).toChar) |
|
78 |
||
79 |
def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") |
|
80 |
||
81 |
||
82 |
/* number */ |
|
83 |
||
84 |
def number: Parser[Token] = |
|
67111
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
85 |
opt("-") ~ number_body ~ opt(letter) ^^ { |
66922 | 86 |
case a ~ b ~ None => Token(Kind.NUMBER, a.getOrElse("") + b) |
87 |
case a ~ b ~ Some(c) => |
|
88 |
errorToken("Invalid number format: " + quote(a.getOrElse("") + b + c)) |
|
89 |
} |
|
90 |
||
91 |
def number_body: Parser[String] = |
|
92 |
(zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ |
|
93 |
{ case a ~ b ~ c => a + b.getOrElse("") + c.getOrElse("") } |
|
94 |
||
95 |
def number_fract: Parser[String] = "." ~ digits1 ^^ { case a ~ b => a + b } |
|
96 |
||
97 |
def number_exp: Parser[String] = |
|
98 |
one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^ |
|
99 |
{ case a ~ b ~ c => a + b + c } |
|
100 |
||
101 |
def zero = one(character(c => c == '0')) |
|
102 |
def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c))) |
|
103 |
def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b } |
|
104 |
||
105 |
||
106 |
/* token */ |
|
107 |
||
108 |
def token: Parser[Token] = |
|
109 |
keyword | (string | (string_failure | (number | failure("Illegal character")))) |
|
110 |
} |
|
111 |
||
112 |
||
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
113 |
/* parser */ |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
114 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
115 |
trait Parser extends Parsers |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
116 |
{ |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
117 |
type Elem = Token |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
118 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
119 |
def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name)) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
120 |
def string: Parser[String] = elem("string", _.is_string) ^^ (_.text) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
121 |
def number: Parser[Double] = elem("number", _.is_number) ^^ (tok => tok.text.toDouble) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
122 |
|
66928 | 123 |
def json_object: Parser[Object] = |
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
124 |
$$$("{") ~> |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
125 |
repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~ |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
126 |
$$$("}") ^^ (_.toMap) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
127 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
128 |
def json_array: Parser[List[T]] = |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
129 |
$$$("[") ~> repsep(json_value, $$$(",")) <~ $$$("]") |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
130 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
131 |
def json_value: Parser[T] = |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
132 |
json_object | (json_array | (number | (string | |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
133 |
($$$("true") ^^^ true | ($$$("false") ^^^ false | ($$$("null") ^^^ null)))))) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
134 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
135 |
def parse(input: CharSequence, strict: Boolean): T = |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
136 |
{ |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
137 |
val scanner = new Lexer.Scanner(Scan.char_reader(input)) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
138 |
phrase(if (strict) json_object | json_array else json_value)(scanner) match { |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
139 |
case Success(json, _) => json |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
140 |
case NoSuccess(_, next) => error("Malformed JSON input at " + next.pos) |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
141 |
} |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
142 |
} |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
143 |
} |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
144 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
145 |
object Parser extends Parser |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
146 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
147 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
148 |
/* standard format */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
149 |
|
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
150 |
def parse(s: S, strict: Boolean = true): T = Parser.parse(s, strict) |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
151 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
152 |
object Format |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
153 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
154 |
def unapply(s: S): Option[T] = |
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
155 |
try { Some(parse(s, strict = false)) } |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
156 |
catch { case ERROR(_) => None } |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
157 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
158 |
def apply(json: T): S = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
159 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
160 |
val result = new StringBuilder |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
161 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
162 |
def string(s: String) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
163 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
164 |
result += '"' |
64761 | 165 |
result ++= |
166 |
s.iterator.map { |
|
167 |
case '"' => "\\\"" |
|
168 |
case '\\' => "\\\\" |
|
169 |
case '\b' => "\\b" |
|
170 |
case '\f' => "\\f" |
|
171 |
case '\n' => "\\n" |
|
172 |
case '\r' => "\\r" |
|
173 |
case '\t' => "\\t" |
|
174 |
case c => |
|
175 |
if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt) |
|
176 |
else c |
|
177 |
}.mkString |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
178 |
result += '"' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
179 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
180 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
181 |
def array(list: List[T]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
182 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
183 |
result += '[' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
184 |
Library.separate(None, list.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
185 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
186 |
case Some(x) => json_format(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
187 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
188 |
result += ']' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
189 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
190 |
|
66928 | 191 |
def object_(obj: Object) |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
192 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
193 |
result += '{' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
194 |
Library.separate(None, obj.toList.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
195 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
196 |
case Some((x, y)) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
197 |
string(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
198 |
result += ':' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
199 |
json_format(y) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
200 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
201 |
result += '}' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
202 |
} |
63644 | 203 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
204 |
def json_format(x: T) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
205 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
206 |
x match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
207 |
case null => result ++= "null" |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
208 |
case _: Int | _: Long | _: Boolean => result ++= x.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
209 |
case n: Double => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
210 |
val i = n.toLong |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
211 |
result ++= (if (i.toDouble == n) i.toString else n.toString) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
212 |
case s: String => string(s) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
213 |
case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) => |
66928 | 214 |
object_(obj.asInstanceOf[Object]) |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
215 |
case list: List[T] => array(list) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
216 |
case _ => error("Bad JSON value: " + x.toString) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
217 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
218 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
219 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
220 |
json_format(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
221 |
result.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
222 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
223 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
224 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
225 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
226 |
/* numbers */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
227 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
228 |
object Number |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
229 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
230 |
object Double { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
231 |
def unapply(json: T): Option[scala.Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
232 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
233 |
case x: scala.Double => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
234 |
case x: scala.Long => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
235 |
case x: scala.Int => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
236 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
237 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
238 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
239 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
240 |
object Long { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
241 |
def unapply(json: T): Option[scala.Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
242 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
243 |
case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
244 |
case x: scala.Long => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
245 |
case x: scala.Int => Some(x.toLong) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
246 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
247 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
248 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
249 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
250 |
object Int { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
251 |
def unapply(json: T): Option[scala.Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
252 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
253 |
case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
254 |
case x: scala.Long if x.toInt.toLong == x => Some(x.toInt) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
255 |
case x: scala.Int => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
256 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
257 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
258 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
259 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
260 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
261 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
262 |
/* object values */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
263 |
|
66928 | 264 |
def optional(entry: (String, Option[T])): Object = |
64878 | 265 |
entry match { |
266 |
case (name, Some(x)) => Map(name -> x) |
|
66926 | 267 |
case (_, None) => empty |
64878 | 268 |
} |
269 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
270 |
def value(obj: T, name: String): Option[T] = |
63644 | 271 |
obj match { |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
272 |
case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => |
66928 | 273 |
m.asInstanceOf[Object].get(name) |
63644 | 274 |
case _ => None |
275 |
} |
|
276 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
277 |
def value[A](obj: T, name: String, unapply: T => Option[A]): Option[A] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
278 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
279 |
json <- value(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
280 |
x <- unapply(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
281 |
} yield x |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
282 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
283 |
def array(obj: T, name: String): Option[List[T]] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
284 |
value(obj, name) match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
285 |
case Some(a: List[T]) => Some(a) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
286 |
case _ => None |
63644 | 287 |
} |
288 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
289 |
def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
290 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
291 |
a0 <- array(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
292 |
a = a0.map(unapply(_)) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
293 |
if a.forall(_.isDefined) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
294 |
} yield a.map(_.get) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
295 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
296 |
def string(obj: T, name: String): Option[String] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
297 |
value(obj, name) match { |
63644 | 298 |
case Some(x: String) => Some(x) |
299 |
case _ => None |
|
300 |
} |
|
301 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
302 |
def double(obj: T, name: String): Option[Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
303 |
value(obj, name, Number.Double.unapply) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
304 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
305 |
def long(obj: T, name: String): Option[Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
306 |
value(obj, name, Number.Long.unapply) |
63644 | 307 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
308 |
def int(obj: T, name: String): Option[Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
309 |
value(obj, name, Number.Int.unapply) |
63644 | 310 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
311 |
def bool(obj: T, name: String): Option[Boolean] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
312 |
value(obj, name) match { |
63644 | 313 |
case Some(x: Boolean) => Some(x) |
314 |
case _ => None |
|
315 |
} |
|
316 |
} |