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