author | wenzelm |
Fri, 27 Oct 2017 13:50:08 +0200 | |
changeset 66924 | b4d4027f743b |
parent 66922 | 5a476a87a535 |
child 66925 | 8b117dc73278 |
permissions | -rw-r--r-- |
63992 | 1 |
/* Title: Pure/General/json.scala |
63644 | 2 |
Author: Makarius |
3 |
||
4 |
Support for JSON parsing. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
66922 | 10 |
import scala.util.parsing.combinator.lexical.Scanners |
11 |
import scala.util.parsing.input.CharArrayReader.EofCh |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
12 |
import scala.util.parsing.json.{JSONObject, JSONArray} |
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 |
|
20 |
||
66922 | 21 |
/* lexer */ |
22 |
||
23 |
object Kind extends Enumeration |
|
24 |
{ |
|
25 |
val KEYWORD, STRING, NUMBER, ERROR = Value |
|
26 |
} |
|
27 |
||
28 |
sealed case class Token(kind: Kind.Value, text: String) |
|
29 |
{ |
|
30 |
def is_keyword: Boolean = kind == Kind.KEYWORD |
|
31 |
def is_string: Boolean = kind == Kind.STRING |
|
32 |
def is_number: Boolean = kind == Kind.NUMBER |
|
33 |
def is_error: Boolean = kind == Kind.ERROR |
|
34 |
} |
|
35 |
||
36 |
object Lexer extends Scanners with Scan.Parsers |
|
37 |
{ |
|
38 |
override type Elem = Char |
|
39 |
type Token = JSON.Token |
|
40 |
||
41 |
def errorToken(msg: String): Token = Token(Kind.ERROR, msg) |
|
42 |
||
43 |
override val whiteSpace = """\s+""".r |
|
44 |
def whitespace: Parser[Any] = many(character(Symbol.is_ascii_blank(_))) |
|
45 |
||
46 |
val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_))) |
|
47 |
val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_))) |
|
48 |
||
49 |
def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_))) |
|
50 |
def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_))) |
|
51 |
||
52 |
||
53 |
/* keyword */ |
|
54 |
||
55 |
def keyword: Parser[Token] = |
|
66924 | 56 |
(letters1 | one(character("{}[],:".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s)) |
66922 | 57 |
|
58 |
||
59 |
/* string */ |
|
60 |
||
61 |
def string: Parser[Token] = |
|
62 |
'\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) |
|
63 |
||
64 |
def string_body: Parser[Char] = |
|
65 |
elem("", c => c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape |
|
66 |
||
67 |
def string_escape: Parser[Char] = |
|
68 |
elem("", "\"\\/".contains(_)) | |
|
69 |
elem("", "bfnrt".contains(_)) ^^ |
|
70 |
{ case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | |
|
71 |
'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ |
|
72 |
(s => Integer.parseInt(s, 16).toChar) |
|
73 |
||
74 |
def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") |
|
75 |
||
76 |
||
77 |
/* number */ |
|
78 |
||
79 |
def number: Parser[Token] = |
|
80 |
opt("-" <~ whitespace) ~ number_body ~ opt(letter) ^^ { |
|
81 |
case a ~ b ~ None => Token(Kind.NUMBER, a.getOrElse("") + b) |
|
82 |
case a ~ b ~ Some(c) => |
|
83 |
errorToken("Invalid number format: " + quote(a.getOrElse("") + b + c)) |
|
84 |
} |
|
85 |
||
86 |
def number_body: Parser[String] = |
|
87 |
(zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ |
|
88 |
{ case a ~ b ~ c => a + b.getOrElse("") + c.getOrElse("") } |
|
89 |
||
90 |
def number_fract: Parser[String] = "." ~ digits1 ^^ { case a ~ b => a + b } |
|
91 |
||
92 |
def number_exp: Parser[String] = |
|
93 |
one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^ |
|
94 |
{ case a ~ b ~ c => a + b + c } |
|
95 |
||
96 |
def zero = one(character(c => c == '0')) |
|
97 |
def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c))) |
|
98 |
def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b } |
|
99 |
||
100 |
||
101 |
/* token */ |
|
102 |
||
103 |
def token: Parser[Token] = |
|
104 |
keyword | (string | (string_failure | (number | failure("Illegal character")))) |
|
105 |
} |
|
106 |
||
107 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
108 |
/* standard format */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
109 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
110 |
def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON") |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
111 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
112 |
object Format |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
113 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
114 |
def unapply(s: S): Option[T] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
115 |
try { scala.util.parsing.json.JSON.parseFull(s) } |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
116 |
catch { case ERROR(_) => None } |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
117 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
118 |
def apply(json: T): S = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
119 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
120 |
val result = new StringBuilder |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
121 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
122 |
def string(s: String) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
123 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
124 |
result += '"' |
64761 | 125 |
result ++= |
126 |
s.iterator.map { |
|
127 |
case '"' => "\\\"" |
|
128 |
case '\\' => "\\\\" |
|
129 |
case '\b' => "\\b" |
|
130 |
case '\f' => "\\f" |
|
131 |
case '\n' => "\\n" |
|
132 |
case '\r' => "\\r" |
|
133 |
case '\t' => "\\t" |
|
134 |
case c => |
|
135 |
if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt) |
|
136 |
else c |
|
137 |
}.mkString |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
138 |
result += '"' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
139 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
140 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
141 |
def array(list: List[T]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
142 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
143 |
result += '[' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
144 |
Library.separate(None, list.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
145 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
146 |
case Some(x) => json_format(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
147 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
148 |
result += ']' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
149 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
150 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
151 |
def object_(obj: Map[String, T]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
152 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
153 |
result += '{' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
154 |
Library.separate(None, obj.toList.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
155 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
156 |
case Some((x, y)) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
157 |
string(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
158 |
result += ':' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
159 |
json_format(y) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
160 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
161 |
result += '}' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
162 |
} |
63644 | 163 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
164 |
def json_format(x: T) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
165 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
166 |
x match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
167 |
case null => result ++= "null" |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
168 |
case _: Int | _: Long | _: Boolean => result ++= x.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
169 |
case n: Double => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
170 |
val i = n.toLong |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
171 |
result ++= (if (i.toDouble == n) i.toString else n.toString) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
172 |
case s: String => string(s) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
173 |
case JSONObject(obj) => object_(obj) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
174 |
case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
175 |
object_(obj.asInstanceOf[Map[String, T]]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
176 |
case JSONArray(list) => array(list) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
177 |
case list: List[T] => array(list) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
178 |
case _ => error("Bad JSON value: " + x.toString) |
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 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
182 |
json_format(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
183 |
result.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
184 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
185 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
186 |
|
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 |
/* numbers */ |
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 |
object Number |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
191 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
192 |
object Double { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
193 |
def unapply(json: T): Option[scala.Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
194 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
195 |
case x: scala.Double => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
196 |
case x: scala.Long => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
197 |
case x: scala.Int => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
198 |
case _ => None |
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 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
201 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
202 |
object Long { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
203 |
def unapply(json: T): Option[scala.Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
204 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
205 |
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
|
206 |
case x: scala.Long => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
207 |
case x: scala.Int => Some(x.toLong) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
208 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
209 |
} |
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 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
212 |
object Int { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
213 |
def unapply(json: T): Option[scala.Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
214 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
215 |
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
|
216 |
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
|
217 |
case x: scala.Int => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
218 |
case _ => None |
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 |
} |
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 |
|
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 |
/* object values */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
225 |
|
64878 | 226 |
def optional(entry: (String, Option[T])): Map[String, T] = |
227 |
entry match { |
|
228 |
case (name, Some(x)) => Map(name -> x) |
|
229 |
case (_, None) => Map.empty |
|
230 |
} |
|
231 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
232 |
def value(obj: T, name: String): Option[T] = |
63644 | 233 |
obj match { |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
234 |
case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
235 |
m.asInstanceOf[Map[String, T]].get(name) |
63644 | 236 |
case _ => None |
237 |
} |
|
238 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
239 |
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
|
240 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
241 |
json <- value(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
242 |
x <- unapply(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
243 |
} yield x |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
244 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
245 |
def array(obj: T, name: String): Option[List[T]] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
246 |
value(obj, name) match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
247 |
case Some(a: List[T]) => Some(a) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
248 |
case _ => None |
63644 | 249 |
} |
250 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
251 |
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
|
252 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
253 |
a0 <- array(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
254 |
a = a0.map(unapply(_)) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
255 |
if a.forall(_.isDefined) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
256 |
} yield a.map(_.get) |
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 |
def string(obj: T, name: String): Option[String] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
259 |
value(obj, name) match { |
63644 | 260 |
case Some(x: String) => Some(x) |
261 |
case _ => None |
|
262 |
} |
|
263 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
264 |
def double(obj: T, name: String): Option[Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
265 |
value(obj, name, Number.Double.unapply) |
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 |
def long(obj: T, name: String): Option[Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
268 |
value(obj, name, Number.Long.unapply) |
63644 | 269 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
270 |
def int(obj: T, name: String): Option[Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
271 |
value(obj, name, Number.Int.unapply) |
63644 | 272 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
273 |
def bool(obj: T, name: String): Option[Boolean] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
274 |
value(obj, name) match { |
63644 | 275 |
case Some(x: Boolean) => Some(x) |
276 |
case _ => None |
|
277 |
} |
|
278 |
} |