author | wenzelm |
Sat, 11 Aug 2018 17:33:00 +0200 | |
changeset 68742 | a6cc4302c380 |
parent 67885 | 839a624aabb9 |
child 68943 | e564605d4cac |
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/. |
67874 | 5 |
|
6 |
See also http://seriot.ch/parsing_json.php "Parsing JSON is a Minefield". |
|
63644 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
12 |
import scala.util.parsing.combinator.Parsers |
66922 | 13 |
import scala.util.parsing.combinator.lexical.Scanners |
14 |
import scala.util.parsing.input.CharArrayReader.EofCh |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
15 |
|
66922 | 16 |
|
63644 | 17 |
object JSON |
18 |
{ |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
19 |
type T = Any |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
20 |
type S = String |
63644 | 21 |
|
67841 | 22 |
object Object |
23 |
{ |
|
67857 | 24 |
type Entry = (String, JSON.T) |
25 |
||
67841 | 26 |
type T = Map[String, JSON.T] |
67850 | 27 |
val empty: Object.T = Map.empty |
28 |
||
67857 | 29 |
def apply(entries: Entry*): Object.T = Map(entries:_*) |
67841 | 30 |
|
31 |
def unapply(obj: T): Option[Object.T] = |
|
32 |
obj match { |
|
33 |
case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => |
|
34 |
Some(m.asInstanceOf[Object.T]) |
|
35 |
case _ => None |
|
36 |
} |
|
37 |
} |
|
66928 | 38 |
|
63644 | 39 |
|
66922 | 40 |
/* lexer */ |
41 |
||
42 |
object Kind extends Enumeration |
|
43 |
{ |
|
44 |
val KEYWORD, STRING, NUMBER, ERROR = Value |
|
45 |
} |
|
46 |
||
47 |
sealed case class Token(kind: Kind.Value, text: String) |
|
48 |
{ |
|
49 |
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
|
50 |
def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name |
66922 | 51 |
def is_string: Boolean = kind == Kind.STRING |
52 |
def is_number: Boolean = kind == Kind.NUMBER |
|
53 |
def is_error: Boolean = kind == Kind.ERROR |
|
54 |
} |
|
55 |
||
56 |
object Lexer extends Scanners with Scan.Parsers |
|
57 |
{ |
|
58 |
override type Elem = Char |
|
59 |
type Token = JSON.Token |
|
60 |
||
61 |
def errorToken(msg: String): Token = Token(Kind.ERROR, msg) |
|
62 |
||
67111
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
63 |
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
|
64 |
override val whiteSpace = ("[" + white_space + "]+").r |
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
65 |
def whitespace: Parser[Any] = many(character(white_space.contains(_))) |
66922 | 66 |
|
67 |
val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_))) |
|
68 |
val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_))) |
|
69 |
||
70 |
def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_))) |
|
71 |
def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_))) |
|
72 |
||
73 |
||
74 |
/* keyword */ |
|
75 |
||
76 |
def keyword: Parser[Token] = |
|
66924 | 77 |
(letters1 | one(character("{}[],:".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s)) |
66922 | 78 |
|
79 |
||
80 |
/* string */ |
|
81 |
||
82 |
def string: Parser[Token] = |
|
83 |
'\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) |
|
84 |
||
85 |
def string_body: Parser[Char] = |
|
67111
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
86 |
elem("", c => c > '\u001f' && c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape |
66922 | 87 |
|
88 |
def string_escape: Parser[Char] = |
|
89 |
elem("", "\"\\/".contains(_)) | |
|
90 |
elem("", "bfnrt".contains(_)) ^^ |
|
91 |
{ case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | |
|
92 |
'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ |
|
93 |
(s => Integer.parseInt(s, 16).toChar) |
|
94 |
||
95 |
def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") |
|
96 |
||
97 |
||
98 |
/* number */ |
|
99 |
||
100 |
def number: Parser[Token] = |
|
67111
42f290d8ccbd
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
wenzelm
parents:
66928
diff
changeset
|
101 |
opt("-") ~ number_body ~ opt(letter) ^^ { |
66922 | 102 |
case a ~ b ~ None => Token(Kind.NUMBER, a.getOrElse("") + b) |
103 |
case a ~ b ~ Some(c) => |
|
104 |
errorToken("Invalid number format: " + quote(a.getOrElse("") + b + c)) |
|
105 |
} |
|
106 |
||
107 |
def number_body: Parser[String] = |
|
108 |
(zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ |
|
109 |
{ case a ~ b ~ c => a + b.getOrElse("") + c.getOrElse("") } |
|
110 |
||
111 |
def number_fract: Parser[String] = "." ~ digits1 ^^ { case a ~ b => a + b } |
|
112 |
||
113 |
def number_exp: Parser[String] = |
|
114 |
one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^ |
|
115 |
{ case a ~ b ~ c => a + b + c } |
|
116 |
||
117 |
def zero = one(character(c => c == '0')) |
|
118 |
def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c))) |
|
119 |
def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b } |
|
120 |
||
121 |
||
122 |
/* token */ |
|
123 |
||
124 |
def token: Parser[Token] = |
|
125 |
keyword | (string | (string_failure | (number | failure("Illegal character")))) |
|
126 |
} |
|
127 |
||
128 |
||
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
129 |
/* parser */ |
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 |
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
|
132 |
{ |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
133 |
type Elem = Token |
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 $$$(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
|
136 |
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
|
137 |
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
|
138 |
|
67841 | 139 |
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
|
140 |
$$$("{") ~> |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
141 |
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
|
142 |
$$$("}") ^^ (_.toMap) |
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 |
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
|
145 |
$$$("[") ~> repsep(json_value, $$$(",")) <~ $$$("]") |
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 |
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
|
148 |
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
|
149 |
($$$("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
|
150 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
151 |
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
|
152 |
{ |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
153 |
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
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
} |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
158 |
} |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
159 |
} |
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
160 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
161 |
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
|
162 |
|
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
163 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
164 |
/* standard format */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
165 |
|
66925
8b117dc73278
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
wenzelm
parents:
66924
diff
changeset
|
166 |
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
|
167 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
168 |
object Format |
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 |
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
|
171 |
try { Some(parse(s, strict = false)) } |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
172 |
catch { case ERROR(_) => None } |
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 |
def apply(json: T): S = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
175 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
176 |
val result = new StringBuilder |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
177 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
178 |
def string(s: String) |
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 |
result += '"' |
64761 | 181 |
result ++= |
182 |
s.iterator.map { |
|
183 |
case '"' => "\\\"" |
|
184 |
case '\\' => "\\\\" |
|
185 |
case '\b' => "\\b" |
|
186 |
case '\f' => "\\f" |
|
187 |
case '\n' => "\\n" |
|
188 |
case '\r' => "\\r" |
|
189 |
case '\t' => "\\t" |
|
190 |
case c => |
|
191 |
if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt) |
|
192 |
else c |
|
193 |
}.mkString |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
194 |
result += '"' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
195 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
196 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
197 |
def array(list: List[T]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
198 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
199 |
result += '[' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
200 |
Library.separate(None, list.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
201 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
202 |
case Some(x) => json_format(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
203 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
204 |
result += ']' |
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 |
|
67841 | 207 |
def object_(obj: Object.T) |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
208 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
209 |
result += '{' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
210 |
Library.separate(None, obj.toList.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
211 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
212 |
case Some((x, y)) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
213 |
string(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
214 |
result += ':' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
215 |
json_format(y) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
216 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
217 |
result += '}' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
218 |
} |
63644 | 219 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
220 |
def json_format(x: T) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
221 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
222 |
x match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
223 |
case null => result ++= "null" |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
224 |
case _: Int | _: Long | _: Boolean => result ++= x.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
225 |
case n: Double => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
226 |
val i = n.toLong |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
227 |
result ++= (if (i.toDouble == n) i.toString else n.toString) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
228 |
case s: String => string(s) |
67841 | 229 |
case Object(m) => object_(m) |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
230 |
case list: List[T] => array(list) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
231 |
case _ => error("Bad JSON value: " + x.toString) |
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 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
235 |
json_format(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
236 |
result.toString |
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 |
|
67843 | 241 |
/* typed values */ |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
242 |
|
67842 | 243 |
object Value |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
244 |
{ |
67885 | 245 |
object UUID |
246 |
{ |
|
247 |
def unapply(json: T): Option[java.util.UUID] = |
|
248 |
json match { |
|
249 |
case x: java.lang.String => |
|
250 |
try { Some(java.util.UUID.fromString(x)) } |
|
251 |
catch { case _: IllegalArgumentException => None } |
|
252 |
case _ => None |
|
253 |
} |
|
254 |
} |
|
255 |
||
67842 | 256 |
object String { |
257 |
def unapply(json: T): Option[java.lang.String] = |
|
258 |
json match { |
|
259 |
case x: java.lang.String => Some(x) |
|
260 |
case _ => None |
|
261 |
} |
|
262 |
} |
|
263 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
264 |
object Double { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
265 |
def unapply(json: T): Option[scala.Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
266 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
267 |
case x: scala.Double => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
268 |
case x: scala.Long => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
269 |
case x: scala.Int => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
270 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
271 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
272 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
273 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
274 |
object Long { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
275 |
def unapply(json: T): Option[scala.Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
276 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
277 |
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
|
278 |
case x: scala.Long => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
279 |
case x: scala.Int => Some(x.toLong) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
280 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
281 |
} |
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 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
284 |
object Int { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
285 |
def unapply(json: T): Option[scala.Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
286 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
287 |
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
|
288 |
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
|
289 |
case x: scala.Int => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
290 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
291 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
292 |
} |
67842 | 293 |
|
294 |
object Boolean { |
|
295 |
def unapply(json: T): Option[scala.Boolean] = |
|
296 |
json match { |
|
297 |
case x: scala.Boolean => Some(x) |
|
298 |
case _ => None |
|
299 |
} |
|
300 |
} |
|
67843 | 301 |
|
302 |
object List |
|
303 |
{ |
|
304 |
def unapply[A](json: T, unapply: T => Option[A]): Option[List[A]] = |
|
305 |
json match { |
|
306 |
case xs: List[T] => |
|
307 |
val ys = xs.map(unapply) |
|
308 |
if (ys.forall(_.isDefined)) Some(ys.map(_.get)) else None |
|
309 |
case _ => None |
|
310 |
} |
|
311 |
} |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
312 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
313 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
314 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
315 |
/* object values */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
316 |
|
67841 | 317 |
def optional(entry: (String, Option[T])): Object.T = |
64878 | 318 |
entry match { |
67850 | 319 |
case (name, Some(x)) => Object(name -> x) |
67841 | 320 |
case (_, None) => Object.empty |
64878 | 321 |
} |
322 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
323 |
def value(obj: T, name: String): Option[T] = |
63644 | 324 |
obj match { |
67841 | 325 |
case Object(m) => m.get(name) |
63644 | 326 |
case _ => None |
327 |
} |
|
328 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
329 |
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
|
330 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
331 |
json <- value(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
332 |
x <- unapply(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
333 |
} yield x |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
334 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
335 |
def array(obj: T, name: String): Option[List[T]] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
336 |
value(obj, name) match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
337 |
case Some(a: List[T]) => Some(a) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
338 |
case _ => None |
63644 | 339 |
} |
340 |
||
67864 | 341 |
def value_default[A](obj: T, name: String, unapply: T => Option[A], default: => A): Option[A] = |
67843 | 342 |
value(obj, name) match { |
343 |
case None => Some(default) |
|
344 |
case Some(json) => unapply(json) |
|
345 |
} |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
346 |
|
67885 | 347 |
def uuid(obj: T, name: String): Option[UUID] = |
348 |
value(obj, name, Value.UUID.unapply) |
|
349 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
350 |
def string(obj: T, name: String): Option[String] = |
67842 | 351 |
value(obj, name, Value.String.unapply) |
67864 | 352 |
def string_default(obj: T, name: String, default: => String = ""): Option[String] = |
67843 | 353 |
value_default(obj, name, Value.String.unapply, default) |
63644 | 354 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
355 |
def double(obj: T, name: String): Option[Double] = |
67842 | 356 |
value(obj, name, Value.Double.unapply) |
67864 | 357 |
def double_default(obj: T, name: String, default: => Double = 0.0): Option[Double] = |
67843 | 358 |
value_default(obj, name, Value.Double.unapply, default) |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
359 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
360 |
def long(obj: T, name: String): Option[Long] = |
67842 | 361 |
value(obj, name, Value.Long.unapply) |
67864 | 362 |
def long_default(obj: T, name: String, default: => Long = 0): Option[Long] = |
67843 | 363 |
value_default(obj, name, Value.Long.unapply, default) |
63644 | 364 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
365 |
def int(obj: T, name: String): Option[Int] = |
67842 | 366 |
value(obj, name, Value.Int.unapply) |
67864 | 367 |
def int_default(obj: T, name: String, default: => Int = 0): Option[Int] = |
67843 | 368 |
value_default(obj, name, Value.Int.unapply, default) |
63644 | 369 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
370 |
def bool(obj: T, name: String): Option[Boolean] = |
67842 | 371 |
value(obj, name, Value.Boolean.unapply) |
67864 | 372 |
def bool_default(obj: T, name: String, default: => Boolean = false): Option[Boolean] = |
67843 | 373 |
value_default(obj, name, Value.Boolean.unapply, default) |
374 |
||
375 |
def list[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = |
|
376 |
value(obj, name, Value.List.unapply(_, unapply)) |
|
67864 | 377 |
def list_default[A](obj: T, name: String, unapply: T => Option[A], default: => List[A] = Nil) |
67843 | 378 |
: Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default) |
68742 | 379 |
|
380 |
def strings(obj: T, name: String): Option[List[String]] = |
|
381 |
list(obj, name, JSON.Value.String.unapply _) |
|
382 |
def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] = |
|
383 |
list_default(obj, name, JSON.Value.String.unapply _, default) |
|
63644 | 384 |
} |