author | wenzelm |
Tue, 12 Jul 2011 20:11:00 +0200 | |
changeset 43783 | ef45eaf2775f |
parent 43781 | d43e5f79bdc2 |
child 43791 | 5e9a1d71f94d |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Pure/General/xml.ML |
24264 | 2 |
Author: David Aspinall, Stefan Berghofer and Markus Wenzel |
3 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
4 |
Untyped XML trees. |
24264 | 5 |
*) |
6 |
||
43767 | 7 |
signature XML_DATA_OPS = |
8 |
sig |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
9 |
type 'a A |
43767 | 10 |
type 'a T |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
11 |
type 'a V |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
12 |
val int_atom: int A |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
13 |
val bool_atom: bool A |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
14 |
val unit_atom: unit A |
43767 | 15 |
val properties: Properties.T T |
16 |
val string: string T |
|
17 |
val int: int T |
|
18 |
val bool: bool T |
|
19 |
val unit: unit T |
|
20 |
val pair: 'a T -> 'b T -> ('a * 'b) T |
|
21 |
val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T |
|
22 |
val list: 'a T -> 'a list T |
|
23 |
val option: 'a T -> 'a option T |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
24 |
val variant: 'a V list -> 'a T |
43767 | 25 |
end; |
26 |
||
24264 | 27 |
signature XML = |
28 |
sig |
|
28017 | 29 |
type attributes = Properties.T |
24264 | 30 |
datatype tree = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
31469
diff
changeset
|
31 |
Elem of Markup.T * tree list |
24264 | 32 |
| Text of string |
38266
492d377ecfe2
type XML.body as basic data representation language;
wenzelm
parents:
38228
diff
changeset
|
33 |
type body = tree list |
26546 | 34 |
val add_content: tree -> Buffer.T -> Buffer.T |
39555
ccb223a4d49c
added XML.content_of convenience -- cover XML.body, which is the general situation;
wenzelm
parents:
38474
diff
changeset
|
35 |
val content_of: body -> string |
26546 | 36 |
val header: string |
37 |
val text: string -> string |
|
38 |
val element: string -> attributes -> string list -> string |
|
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39555
diff
changeset
|
39 |
val output_markup: Markup.T -> Output.output * Output.output |
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
40 |
val string_of: tree -> string |
26546 | 41 |
val output: tree -> TextIO.outstream -> unit |
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
42 |
val parse_comments: string list -> unit * string list |
24264 | 43 |
val parse_string : string -> string option |
26546 | 44 |
val parse_element: string list -> tree * string list |
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
45 |
val parse_document: string list -> tree * string list |
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
46 |
val parse: string -> tree |
43767 | 47 |
exception XML_ATOM of string |
48 |
exception XML_BODY of body |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
49 |
structure Encode: XML_DATA_OPS |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
50 |
structure Decode: XML_DATA_OPS |
24264 | 51 |
end; |
52 |
||
53 |
structure XML: XML = |
|
54 |
struct |
|
55 |
||
26546 | 56 |
(** XML trees **) |
57 |
||
28017 | 58 |
type attributes = Properties.T; |
26546 | 59 |
|
60 |
datatype tree = |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
31469
diff
changeset
|
61 |
Elem of Markup.T * tree list |
28033 | 62 |
| Text of string; |
26546 | 63 |
|
38266
492d377ecfe2
type XML.body as basic data representation language;
wenzelm
parents:
38228
diff
changeset
|
64 |
type body = tree list; |
492d377ecfe2
type XML.body as basic data representation language;
wenzelm
parents:
38228
diff
changeset
|
65 |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
31469
diff
changeset
|
66 |
fun add_content (Elem (_, ts)) = fold add_content ts |
28033 | 67 |
| add_content (Text s) = Buffer.add s; |
26546 | 68 |
|
39555
ccb223a4d49c
added XML.content_of convenience -- cover XML.body, which is the general situation;
wenzelm
parents:
38474
diff
changeset
|
69 |
fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content; |
ccb223a4d49c
added XML.content_of convenience -- cover XML.body, which is the general situation;
wenzelm
parents:
38474
diff
changeset
|
70 |
|
26546 | 71 |
|
24264 | 72 |
|
26525 | 73 |
(** string representation **) |
74 |
||
24264 | 75 |
val header = "<?xml version=\"1.0\"?>\n"; |
76 |
||
77 |
||
26546 | 78 |
(* escaped text *) |
24264 | 79 |
|
80 |
fun decode "<" = "<" |
|
81 |
| decode ">" = ">" |
|
82 |
| decode "&" = "&" |
|
83 |
| decode "'" = "'" |
|
84 |
| decode """ = "\"" |
|
85 |
| decode c = c; |
|
86 |
||
87 |
fun encode "<" = "<" |
|
88 |
| encode ">" = ">" |
|
89 |
| encode "&" = "&" |
|
90 |
| encode "'" = "'" |
|
91 |
| encode "\"" = """ |
|
92 |
| encode c = c; |
|
93 |
||
25838 | 94 |
val text = translate_string encode; |
24264 | 95 |
|
96 |
||
97 |
(* elements *) |
|
98 |
||
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
99 |
fun elem name atts = |
26551 | 100 |
space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts); |
24264 | 101 |
|
26525 | 102 |
fun element name atts body = |
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
103 |
let val b = implode body in |
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
104 |
if b = "" then enclose "<" "/>" (elem name atts) |
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
105 |
else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name |
24264 | 106 |
end; |
107 |
||
27884 | 108 |
fun output_markup (markup as (name, atts)) = |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38266
diff
changeset
|
109 |
if Markup.is_empty markup then Markup.no_output |
27884 | 110 |
else (enclose "<" ">" (elem name atts), enclose "</" ">" name); |
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
111 |
|
24264 | 112 |
|
26546 | 113 |
(* output *) |
24264 | 114 |
|
26546 | 115 |
fun buffer_of tree = |
24264 | 116 |
let |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
31469
diff
changeset
|
117 |
fun traverse (Elem ((name, atts), [])) = |
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
118 |
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>" |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
31469
diff
changeset
|
119 |
| traverse (Elem ((name, atts), ts)) = |
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
120 |
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #> |
26546 | 121 |
fold traverse ts #> |
26525 | 122 |
Buffer.add "</" #> Buffer.add name #> Buffer.add ">" |
28033 | 123 |
| traverse (Text s) = Buffer.add (text s); |
26546 | 124 |
in Buffer.empty |> traverse tree end; |
24264 | 125 |
|
26546 | 126 |
val string_of = Buffer.content o buffer_of; |
127 |
val output = Buffer.output o buffer_of; |
|
25838 | 128 |
|
24264 | 129 |
|
130 |
||
26546 | 131 |
(** XML parsing (slow) **) |
132 |
||
133 |
local |
|
24264 | 134 |
|
135 |
fun err s (xs, _) = |
|
136 |
"XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs); |
|
137 |
||
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
138 |
fun ignored _ = []; |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
139 |
|
26551 | 140 |
val blanks = Scan.many Symbol.is_blank; |
141 |
val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode; |
|
142 |
val regular = Scan.one Symbol.is_regular; |
|
143 |
fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x); |
|
24264 | 144 |
|
26551 | 145 |
val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode; |
24264 | 146 |
|
26551 | 147 |
val parse_cdata = |
148 |
Scan.this_string "<![CDATA[" |-- |
|
149 |
(Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --| |
|
150 |
Scan.this_string "]]>"; |
|
24264 | 151 |
|
152 |
val parse_att = |
|
26551 | 153 |
(Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) -- |
154 |
(($$ "\"" || $$ "'") :|-- (fn s => |
|
155 |
(Scan.repeat (special || regular_except s) >> implode) --| $$ s)); |
|
24264 | 156 |
|
26551 | 157 |
val parse_comment = |
158 |
Scan.this_string "<!--" -- |
|
159 |
Scan.repeat (Scan.unless (Scan.this_string "-->") regular) -- |
|
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
160 |
Scan.this_string "-->" >> ignored; |
24264 | 161 |
|
26551 | 162 |
val parse_processing_instruction = |
163 |
Scan.this_string "<?" -- |
|
164 |
Scan.repeat (Scan.unless (Scan.this_string "?>") regular) -- |
|
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
165 |
Scan.this_string "?>" >> ignored; |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
166 |
|
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
167 |
val parse_doctype = |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
168 |
Scan.this_string "<!DOCTYPE" -- |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
169 |
Scan.repeat (Scan.unless ($$ ">") regular) -- |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
170 |
$$ ">" >> ignored; |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
171 |
|
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
172 |
val parse_misc = |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
173 |
Scan.one Symbol.is_blank >> ignored || |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
174 |
parse_processing_instruction || |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
175 |
parse_comment; |
26551 | 176 |
|
177 |
val parse_optional_text = |
|
178 |
Scan.optional (parse_chars >> (single o Text)) []; |
|
24264 | 179 |
|
26546 | 180 |
in |
181 |
||
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
182 |
val parse_comments = |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
183 |
blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K (); |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
184 |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40131
diff
changeset
|
185 |
val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode; |
26546 | 186 |
|
24264 | 187 |
fun parse_content xs = |
26551 | 188 |
(parse_optional_text @@@ |
189 |
(Scan.repeat |
|
190 |
((parse_element >> single || |
|
191 |
parse_cdata >> (single o Text) || |
|
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
192 |
parse_processing_instruction || |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
193 |
parse_comment) |
26551 | 194 |
@@@ parse_optional_text) >> flat)) xs |
24264 | 195 |
|
26546 | 196 |
and parse_element xs = |
24264 | 197 |
($$ "<" |-- Symbol.scan_id -- |
26551 | 198 |
Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (s, _) => |
24264 | 199 |
!! (err "Expected > or />") |
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
200 |
(Scan.this_string "/>" >> ignored |
24264 | 201 |
|| $$ ">" |-- parse_content --| |
202 |
!! (err ("Expected </" ^ s ^ ">")) |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
31469
diff
changeset
|
203 |
(Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs; |
24264 | 204 |
|
26984
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
205 |
val parse_document = |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
206 |
(Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc) |
d0e098e206f3
added parse_document (optional unchecked header material);
wenzelm
parents:
26554
diff
changeset
|
207 |
|-- parse_element; |
24264 | 208 |
|
26539
a0754be538ab
added output_markup (from Tools/isabelle_process.ML);
wenzelm
parents:
26525
diff
changeset
|
209 |
fun parse s = |
24264 | 210 |
(case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element") |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40131
diff
changeset
|
211 |
(blanks |-- parse_document --| blanks))) (raw_explode s) of |
24264 | 212 |
(x, []) => x |
213 |
| (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys)); |
|
214 |
||
215 |
end; |
|
26546 | 216 |
|
43767 | 217 |
|
218 |
||
219 |
(** XML as data representation language **) |
|
220 |
||
221 |
exception XML_ATOM of string; |
|
222 |
exception XML_BODY of tree list; |
|
223 |
||
224 |
||
225 |
structure Encode = |
|
226 |
struct |
|
227 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
228 |
type 'a A = 'a -> string; |
43767 | 229 |
type 'a T = 'a -> body; |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
230 |
type 'a V = 'a -> string list * body; |
43767 | 231 |
|
232 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
233 |
(* atomic values *) |
43767 | 234 |
|
235 |
fun int_atom i = signed_string_of_int i; |
|
236 |
||
237 |
fun bool_atom false = "0" |
|
238 |
| bool_atom true = "1"; |
|
239 |
||
240 |
fun unit_atom () = ""; |
|
241 |
||
242 |
||
243 |
(* structural nodes *) |
|
244 |
||
245 |
fun node ts = Elem ((":", []), ts); |
|
246 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
247 |
fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs; |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
248 |
|
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
249 |
fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts); |
43767 | 250 |
|
251 |
||
252 |
(* representation of standard types *) |
|
253 |
||
254 |
fun properties props = [Elem ((":", props), [])]; |
|
255 |
||
256 |
fun string "" = [] |
|
257 |
| string s = [Text s]; |
|
258 |
||
259 |
val int = string o int_atom; |
|
260 |
||
261 |
val bool = string o bool_atom; |
|
262 |
||
263 |
val unit = string o unit_atom; |
|
264 |
||
265 |
fun pair f g (x, y) = [node (f x), node (g y)]; |
|
266 |
||
267 |
fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]; |
|
268 |
||
269 |
fun list f xs = map (node o f) xs; |
|
270 |
||
271 |
fun option _ NONE = [] |
|
272 |
| option f (SOME x) = [node (f x)]; |
|
273 |
||
274 |
fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))]; |
|
275 |
||
26546 | 276 |
end; |
43767 | 277 |
|
278 |
||
279 |
structure Decode = |
|
280 |
struct |
|
281 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
282 |
type 'a A = string -> 'a; |
43767 | 283 |
type 'a T = body -> 'a; |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
284 |
type 'a V = string list * body -> 'a; |
43767 | 285 |
|
286 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
287 |
(* atomic values *) |
43767 | 288 |
|
289 |
fun int_atom s = |
|
290 |
(case Int.fromString s of |
|
291 |
SOME i => i |
|
292 |
| NONE => raise XML_ATOM s); |
|
293 |
||
294 |
fun bool_atom "0" = false |
|
295 |
| bool_atom "1" = true |
|
296 |
| bool_atom s = raise XML_ATOM s; |
|
297 |
||
298 |
fun unit_atom "" = () |
|
299 |
| unit_atom s = raise XML_ATOM s; |
|
300 |
||
301 |
||
302 |
(* structural nodes *) |
|
303 |
||
304 |
fun node (Elem ((":", []), ts)) = ts |
|
305 |
| node t = raise XML_BODY [t]; |
|
306 |
||
43783 | 307 |
fun vector atts = |
308 |
fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts; |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
309 |
|
43781 | 310 |
fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts)) |
43767 | 311 |
| tagged t = raise XML_BODY [t]; |
312 |
||
313 |
||
314 |
(* representation of standard types *) |
|
315 |
||
316 |
fun properties [Elem ((":", props), [])] = props |
|
317 |
| properties ts = raise XML_BODY ts; |
|
318 |
||
319 |
fun string [] = "" |
|
320 |
| string [Text s] = s |
|
321 |
| string ts = raise XML_BODY ts; |
|
322 |
||
323 |
val int = int_atom o string; |
|
324 |
||
325 |
val bool = bool_atom o string; |
|
326 |
||
327 |
val unit = unit_atom o string; |
|
328 |
||
329 |
fun pair f g [t1, t2] = (f (node t1), g (node t2)) |
|
330 |
| pair _ _ ts = raise XML_BODY ts; |
|
331 |
||
332 |
fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3)) |
|
333 |
| triple _ _ _ ts = raise XML_BODY ts; |
|
334 |
||
335 |
fun list f ts = map (f o node) ts; |
|
336 |
||
337 |
fun option _ [] = NONE |
|
338 |
| option f [t] = SOME (f (node t)) |
|
339 |
| option _ ts = raise XML_BODY ts; |
|
340 |
||
43768 | 341 |
fun variant fs [t] = |
342 |
let |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
343 |
val (tag, (xs, ts)) = tagged t; |
43768 | 344 |
val f = nth fs tag handle General.Subscript => raise XML_BODY [t]; |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
345 |
in f (xs, ts) end |
43767 | 346 |
| variant _ ts = raise XML_BODY ts; |
347 |
||
348 |
end; |
|
349 |
||
350 |
end; |