author | wenzelm |
Sun, 30 Apr 2017 09:23:03 +0200 | |
changeset 65641 | 3b0110e25745 |
parent 64878 | e9208a9301c0 |
child 66922 | 5a476a87a535 |
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 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
10 |
import scala.util.parsing.json.{JSONObject, JSONArray} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
11 |
|
63644 | 12 |
object JSON |
13 |
{ |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
14 |
type T = Any |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
15 |
type S = String |
63644 | 16 |
|
17 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
18 |
/* standard format */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
19 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
20 |
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
|
21 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
22 |
object Format |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
23 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
24 |
def unapply(s: S): Option[T] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
25 |
try { scala.util.parsing.json.JSON.parseFull(s) } |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
26 |
catch { case ERROR(_) => None } |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
27 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
28 |
def apply(json: T): S = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
29 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
30 |
val result = new StringBuilder |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
31 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
32 |
def string(s: String) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
33 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
34 |
result += '"' |
64761 | 35 |
result ++= |
36 |
s.iterator.map { |
|
37 |
case '"' => "\\\"" |
|
38 |
case '\\' => "\\\\" |
|
39 |
case '\b' => "\\b" |
|
40 |
case '\f' => "\\f" |
|
41 |
case '\n' => "\\n" |
|
42 |
case '\r' => "\\r" |
|
43 |
case '\t' => "\\t" |
|
44 |
case c => |
|
45 |
if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt) |
|
46 |
else c |
|
47 |
}.mkString |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
48 |
result += '"' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
49 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
50 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
51 |
def array(list: List[T]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
52 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
53 |
result += '[' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
54 |
Library.separate(None, list.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
55 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
56 |
case Some(x) => json_format(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
57 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
58 |
result += ']' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
59 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
60 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
61 |
def object_(obj: Map[String, T]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
62 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
63 |
result += '{' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
64 |
Library.separate(None, obj.toList.map(Some(_))).foreach({ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
65 |
case None => result += ',' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
66 |
case Some((x, y)) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
67 |
string(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
68 |
result += ':' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
69 |
json_format(y) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
70 |
}) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
71 |
result += '}' |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
72 |
} |
63644 | 73 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
74 |
def json_format(x: T) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
75 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
76 |
x match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
77 |
case null => result ++= "null" |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
78 |
case _: Int | _: Long | _: Boolean => result ++= x.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
79 |
case n: Double => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
80 |
val i = n.toLong |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
81 |
result ++= (if (i.toDouble == n) i.toString else n.toString) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
82 |
case s: String => string(s) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
83 |
case JSONObject(obj) => object_(obj) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
84 |
case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
85 |
object_(obj.asInstanceOf[Map[String, T]]) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
86 |
case JSONArray(list) => array(list) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
87 |
case list: List[T] => array(list) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
88 |
case _ => error("Bad JSON value: " + x.toString) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
89 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
90 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
91 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
92 |
json_format(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
93 |
result.toString |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
94 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
95 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
96 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
97 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
98 |
/* numbers */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
99 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
100 |
object Number |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
101 |
{ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
102 |
object Double { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
103 |
def unapply(json: T): Option[scala.Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
104 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
105 |
case x: scala.Double => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
106 |
case x: scala.Long => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
107 |
case x: scala.Int => Some(x.toDouble) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
108 |
case _ => None |
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 |
} |
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 Long { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
113 |
def unapply(json: T): Option[scala.Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
114 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
115 |
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
|
116 |
case x: scala.Long => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
117 |
case x: scala.Int => Some(x.toLong) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
118 |
case _ => None |
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 |
} |
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 |
object Int { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
123 |
def unapply(json: T): Option[scala.Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
124 |
json match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
125 |
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
|
126 |
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
|
127 |
case x: scala.Int => Some(x) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
128 |
case _ => None |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
129 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
130 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
131 |
} |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
132 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
133 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
134 |
/* object values */ |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
135 |
|
64878 | 136 |
def optional(entry: (String, Option[T])): Map[String, T] = |
137 |
entry match { |
|
138 |
case (name, Some(x)) => Map(name -> x) |
|
139 |
case (_, None) => Map.empty |
|
140 |
} |
|
141 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
142 |
def value(obj: T, name: String): Option[T] = |
63644 | 143 |
obj match { |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
144 |
case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
145 |
m.asInstanceOf[Map[String, T]].get(name) |
63644 | 146 |
case _ => None |
147 |
} |
|
148 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
149 |
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
|
150 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
151 |
json <- value(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
152 |
x <- unapply(json) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
153 |
} yield x |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
154 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
155 |
def array(obj: T, name: String): Option[List[T]] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
156 |
value(obj, name) match { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
157 |
case Some(a: List[T]) => Some(a) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
158 |
case _ => None |
63644 | 159 |
} |
160 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
161 |
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
|
162 |
for { |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
163 |
a0 <- array(obj, name) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
164 |
a = a0.map(unapply(_)) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
165 |
if a.forall(_.isDefined) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
166 |
} yield a.map(_.get) |
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 string(obj: T, name: String): Option[String] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
169 |
value(obj, name) match { |
63644 | 170 |
case Some(x: String) => Some(x) |
171 |
case _ => None |
|
172 |
} |
|
173 |
||
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
174 |
def double(obj: T, name: String): Option[Double] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
175 |
value(obj, name, Number.Double.unapply) |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
176 |
|
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
177 |
def long(obj: T, name: String): Option[Long] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
178 |
value(obj, name, Number.Long.unapply) |
63644 | 179 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
180 |
def int(obj: T, name: String): Option[Int] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
181 |
value(obj, name, Number.Int.unapply) |
63644 | 182 |
|
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
183 |
def bool(obj: T, name: String): Option[Boolean] = |
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
63992
diff
changeset
|
184 |
value(obj, name) match { |
63644 | 185 |
case Some(x: Boolean) => Some(x) |
186 |
case _ => None |
|
187 |
} |
|
188 |
} |