--- a/src/Pure/General/xml.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/General/xml.ML Sat Aug 07 21:03:06 2010 +0200
@@ -1,14 +1,14 @@
(* Title: Pure/General/xml.ML
Author: David Aspinall, Stefan Berghofer and Markus Wenzel
-Basic support for XML.
+Simple XML tree values.
*)
signature XML =
sig
type attributes = Properties.T
datatype tree =
- Elem of string * attributes * tree list
+ Elem of Markup.T * tree list
| Text of string
val add_content: tree -> Buffer.T -> Buffer.T
val header: string
@@ -32,10 +32,10 @@
type attributes = Properties.T;
datatype tree =
- Elem of string * attributes * tree list
+ Elem of Markup.T * tree list
| Text of string;
-fun add_content (Elem (_, _, ts)) = fold add_content ts
+fun add_content (Elem (_, ts)) = fold add_content ts
| add_content (Text s) = Buffer.add s;
@@ -84,9 +84,9 @@
fun buffer_of tree =
let
- fun traverse (Elem (name, atts, [])) =
+ fun traverse (Elem ((name, atts), [])) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
- | traverse (Elem (name, atts, ts)) =
+ | traverse (Elem ((name, atts), ts)) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
fold traverse ts #>
Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
@@ -170,8 +170,7 @@
(Scan.this_string "/>" >> ignored
|| $$ ">" |-- parse_content --|
!! (err ("Expected </" ^ s ^ ">"))
- (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >>
- (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
+ (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
val parse_document =
(Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
--- a/src/Pure/General/yxml.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/General/yxml.ML Sat Aug 07 21:03:06 2010 +0200
@@ -64,7 +64,7 @@
fun attrib (a, x) =
Buffer.add Y #>
Buffer.add a #> Buffer.add "=" #> Buffer.add x;
- fun tree (XML.Elem (name, atts, ts)) =
+ fun tree (XML.Elem ((name, atts), ts)) =
Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
fold tree ts #>
Buffer.add XYX
@@ -104,7 +104,7 @@
| push name atts pending = ((name, atts), []) :: pending;
fun pop ((("", _), _) :: _) = err_unbalanced ""
- | pop (((name, atts), body) :: pending) = add (XML.Elem (name, atts, rev body)) pending;
+ | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
(* parsing *)
--- a/src/Pure/Isar/token.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/Isar/token.ML Sat Aug 07 21:03:06 2010 +0200
@@ -181,7 +181,7 @@
(* token content *)
fun source_of (Token ((source, (pos, _)), _, _)) =
- YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
+ YXML.string_of (XML.Elem ((Markup.tokenN, Position.properties_of pos), [XML.Text source]));
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Sat Aug 07 21:03:06 2010 +0200
@@ -22,7 +22,7 @@
endLine = end_line, endPosition = end_offset} = loc;
val loc_props =
(case YXML.parse text of
- XML.Elem (e, atts, _) => if e = Markup.positionN then atts else []
+ XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
| XML.Text s => Position.file_name s);
in
Position.value Markup.lineN line @
--- a/src/Pure/ProofGeneral/pgip_input.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML Sat Aug 07 21:03:06 2010 +0200
@@ -62,7 +62,7 @@
(* unofficial escape command for debugging *)
| Quitpgip of { }
- val input: string * XML.attributes * XML.tree list -> pgipinput option (* raises PGIP *)
+ val input: Markup.T * XML.tree list -> pgipinput option (* raises PGIP *)
end
structure PgipInput : PGIPINPUT =
@@ -161,7 +161,7 @@
Raise PGIP exception for invalid data.
Return NONE for unknown/unhandled commands.
*)
-fun input (elem, attrs, data) =
+fun input ((elem, attrs), data) =
SOME
(case elem of
"askpgip" => Askpgip { }
--- a/src/Pure/ProofGeneral/pgip_markup.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Sat Aug 07 21:03:06 2010 +0200
@@ -75,81 +75,81 @@
case docelt of
Openblock vs =>
- XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
- opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
- opt_attr "metavarid" (#metavarid vs),
+ XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
+ opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
+ opt_attr "metavarid" (#metavarid vs)),
[])
| Closeblock _ =>
- XML.Elem("closeblock", [], [])
+ XML.Elem(("closeblock", []), [])
| Opentheory vs =>
- XML.Elem("opentheory",
+ XML.Elem(("opentheory",
opt_attr "thyname" (#thyname vs) @
opt_attr "parentnames"
(case (#parentnames vs)
of [] => NONE
- | ps => SOME (space_implode ";" ps)),
+ | ps => SOME (space_implode ";" ps))),
[XML.Text (#text vs)])
| Theoryitem vs =>
- XML.Elem("theoryitem",
+ XML.Elem(("theoryitem",
opt_attr "name" (#name vs) @
- opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
+ opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs)),
[XML.Text (#text vs)])
| Closetheory vs =>
- XML.Elem("closetheory", [], [XML.Text (#text vs)])
+ XML.Elem(("closetheory", []), [XML.Text (#text vs)])
| Opengoal vs =>
- XML.Elem("opengoal",
- opt_attr "thmname" (#thmname vs),
+ XML.Elem(("opengoal",
+ opt_attr "thmname" (#thmname vs)),
[XML.Text (#text vs)])
| Proofstep vs =>
- XML.Elem("proofstep", [], [XML.Text (#text vs)])
+ XML.Elem(("proofstep", []), [XML.Text (#text vs)])
| Closegoal vs =>
- XML.Elem("closegoal", [], [XML.Text (#text vs)])
+ XML.Elem(("closegoal", []), [XML.Text (#text vs)])
| Giveupgoal vs =>
- XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
+ XML.Elem(("giveupgoal", []), [XML.Text (#text vs)])
| Postponegoal vs =>
- XML.Elem("postponegoal", [], [XML.Text (#text vs)])
+ XML.Elem(("postponegoal", []), [XML.Text (#text vs)])
| Comment vs =>
- XML.Elem("comment", [], [XML.Text (#text vs)])
+ XML.Elem(("comment", []), [XML.Text (#text vs)])
| Whitespace vs =>
- XML.Elem("whitespace", [], [XML.Text (#text vs)])
+ XML.Elem(("whitespace", []), [XML.Text (#text vs)])
| Doccomment vs =>
- XML.Elem("doccomment", [], [XML.Text (#text vs)])
+ XML.Elem(("doccomment", []), [XML.Text (#text vs)])
| Spuriouscmd vs =>
- XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
+ XML.Elem(("spuriouscmd", []), [XML.Text (#text vs)])
| Badcmd vs =>
- XML.Elem("badcmd", [], [XML.Text (#text vs)])
+ XML.Elem(("badcmd", []), [XML.Text (#text vs)])
| Unparseable vs =>
- XML.Elem("unparseable", [], [XML.Text (#text vs)])
+ XML.Elem(("unparseable", []), [XML.Text (#text vs)])
| Metainfo vs =>
- XML.Elem("metainfo", opt_attr "name" (#name vs),
+ XML.Elem(("metainfo", opt_attr "name" (#name vs)),
[XML.Text (#text vs)])
| Litcomment vs =>
- XML.Elem("litcomment", opt_attr "format" (#format vs),
+ XML.Elem(("litcomment", opt_attr "format" (#format vs)),
#content vs)
| Showcode vs =>
- XML.Elem("showcode",
- attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
+ XML.Elem(("showcode",
+ attr "show" (PgipTypes.bool_to_pgstring (#show vs))), [])
| Setformat vs =>
- XML.Elem("setformat", attr "format" (#format vs), [])
+ XML.Elem(("setformat", attr "format" (#format vs)), [])
val output_doc = map xml_of
--- a/src/Pure/ProofGeneral/pgip_output.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML Sat Aug 07 21:03:06 2010 +0200
@@ -117,9 +117,7 @@
let
val content = #content vs
in
- XML.Elem ("normalresponse",
- [],
- content)
+ XML.Elem (("normalresponse", []), content)
end
fun errorresponse (Errorresponse vs) =
@@ -128,9 +126,9 @@
val location = #location vs
val content = #content vs
in
- XML.Elem ("errorresponse",
+ XML.Elem (("errorresponse",
attrs_of_fatality fatality @
- these (Option.map attrs_of_location location),
+ these (Option.map attrs_of_location location)),
content)
end
@@ -139,9 +137,9 @@
val url = #url vs
val completed = #completed vs
in
- XML.Elem ("informfileloaded",
+ XML.Elem (("informfileloaded",
attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+ (attr "completed" (PgipTypes.bool_to_pgstring completed))),
[])
end
@@ -150,9 +148,9 @@
val url = #url vs
val completed = #completed vs
in
- XML.Elem ("informfileoutdated",
+ XML.Elem (("informfileoutdated",
attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+ (attr "completed" (PgipTypes.bool_to_pgstring completed))),
[])
end
@@ -161,9 +159,9 @@
val url = #url vs
val completed = #completed vs
in
- XML.Elem ("informfileretracted",
+ XML.Elem (("informfileretracted",
attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+ (attr "completed" (PgipTypes.bool_to_pgstring completed))),
[])
end
@@ -172,14 +170,14 @@
val attrs = #attrs vs
val content = #content vs
in
- XML.Elem ("metainforesponse", attrs, content)
+ XML.Elem (("metainforesponse", attrs), content)
end
fun lexicalstructure (Lexicalstructure vs) =
let
val content = #content vs
in
- XML.Elem ("lexicalstructure", [], content)
+ XML.Elem (("lexicalstructure", []), content)
end
fun proverinfo (Proverinfo vs) =
@@ -191,13 +189,13 @@
val url = #url vs
val filenameextns = #filenameextns vs
in
- XML.Elem ("proverinfo",
+ XML.Elem (("proverinfo",
[("name", name),
("version", version),
("instance", instance),
("descr", descr),
("url", Url.implode url),
- ("filenameextns", filenameextns)],
+ ("filenameextns", filenameextns)]),
[])
end
@@ -205,7 +203,7 @@
let
val idtables = #idtables vs
in
- XML.Elem ("setids",[],map idtable_to_xml idtables)
+ XML.Elem (("setids", []), map idtable_to_xml idtables)
end
fun setrefs (Setrefs vs) =
@@ -216,13 +214,13 @@
val name = #name vs
val idtables = #idtables vs
val fileurls = #fileurls vs
- fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
+ fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
in
- XML.Elem ("setrefs",
+ XML.Elem (("setrefs",
(the_default [] (Option.map attrs_of_pgipurl url)) @
(the_default [] (Option.map attrs_of_objtype objtype)) @
(opt_attr "thyname" thyname) @
- (opt_attr "name" name),
+ (opt_attr "name" name)),
(map idtable_to_xml idtables) @
(map fileurl_to_xml fileurls))
end
@@ -231,14 +229,14 @@
let
val idtables = #idtables vs
in
- XML.Elem ("addids",[],map idtable_to_xml idtables)
+ XML.Elem (("addids", []), map idtable_to_xml idtables)
end
fun delids (Delids vs) =
let
val idtables = #idtables vs
in
- XML.Elem ("delids",[],map idtable_to_xml idtables)
+ XML.Elem (("delids", []), map idtable_to_xml idtables)
end
fun hasprefs (Hasprefs vs) =
@@ -246,7 +244,7 @@
val prefcategory = #prefcategory vs
val prefs = #prefs vs
in
- XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
+ XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
end
fun prefval (Prefval vs) =
@@ -254,7 +252,7 @@
val name = #name vs
val value = #value vs
in
- XML.Elem("prefval", attr "name" name, [XML.Text value])
+ XML.Elem (("prefval", attr "name" name), [XML.Text value])
end
fun idvalue (Idvalue vs) =
@@ -264,10 +262,10 @@
val name = #name vs
val text = #text vs
in
- XML.Elem("idvalue",
+ XML.Elem (("idvalue",
objtype_attrs @
(opt_attr "thyname" thyname) @
- (attr "name" name),
+ attr "name" name),
text)
end
@@ -278,7 +276,7 @@
val theorem = #theorem vs
val proofpos = #proofpos vs
- fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])]
+ fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
val guisefile = elto "guisefile" attrs_of_pgipurl file
val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
@@ -286,7 +284,7 @@
(fn thm=>(attr "thmname" thm) @
(opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
in
- XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
+ XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
end
fun parseresult (Parseresult vs) =
@@ -296,7 +294,7 @@
val errs = #errs vs
val xmldoc = PgipMarkup.output_doc doc
in
- XML.Elem("parseresult", attrs, errs @ xmldoc)
+ XML.Elem (("parseresult", attrs), errs @ xmldoc)
end
fun acceptedpgipelems (Usespgip vs) =
@@ -305,11 +303,10 @@
fun async_attrs b = if b then attr "async" "true" else []
fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
fun singlepgipelem (e,async,attrs) =
- XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e])
+ XML.Elem (("pgipelem", async_attrs async @ attrs_attrs attrs), [XML.Text e])
in
- XML.Elem ("acceptedpgipelems", [],
- map singlepgipelem pgipelems)
+ XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
end
fun usespgip (Usespgip vs) =
@@ -317,14 +314,14 @@
val version = #version vs
val acceptedelems = acceptedpgipelems (Usespgip vs)
in
- XML.Elem("usespgip", attr "version" version, [acceptedelems])
+ XML.Elem (("usespgip", attr "version" version), [acceptedelems])
end
fun usespgml (Usespgml vs) =
let
val version = #version vs
in
- XML.Elem("usespgml", attr "version" version, [])
+ XML.Elem (("usespgml", attr "version" version), [])
end
fun pgip (Pgip vs) =
@@ -338,18 +335,18 @@
val refseq = #refseq vs
val content = #content vs
in
- XML.Elem("pgip",
+ XML.Elem(("pgip",
opt_attr "tag" tag @
attr "id" id @
opt_attr "destid" destid @
attr "class" class @
opt_attr "refid" refid @
opt_attr_map string_of_int "refseq" refseq @
- attr "seq" (string_of_int seq),
+ attr "seq" (string_of_int seq)),
content)
end
-fun ready (Ready _) = XML.Elem("ready",[],[])
+fun ready (Ready _) = XML.Elem (("ready", []), [])
fun output pgipoutput = case pgipoutput of
--- a/src/Pure/ProofGeneral/pgip_types.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML Sat Aug 07 21:03:06 2010 +0200
@@ -168,11 +168,9 @@
let
val objtype_attrs = attrs_of_objtype objtype
val context_attrs = opt_attr "context" context
- val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
+ val ids_content = map (fn x => XML.Elem(("identifier", []), [XML.Text x])) ids
in
- XML.Elem ("idtable",
- objtype_attrs @ context_attrs,
- ids_content)
+ XML.Elem (("idtable", objtype_attrs @ context_attrs), ids_content)
end
@@ -282,7 +280,7 @@
Pgipchoice ds => map destpgipdtype ds
| _ => []
in
- XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
+ XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs)
end
val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
@@ -424,10 +422,10 @@
pgiptype: pgiptype }
fun haspref ({ name, descr, default, pgiptype}:preference) =
- XML.Elem ("haspref",
+ XML.Elem (("haspref",
attr "name" name @
opt_attr "descr" descr @
- opt_attr "default" default,
+ opt_attr "default" default),
[pgiptype_to_xml pgiptype])
end
--- a/src/Pure/ProofGeneral/pgml.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML Sat Aug 07 21:03:06 2010 +0200
@@ -109,25 +109,25 @@
(* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
would be better not to *) (* FIXME !??? *)
- fun atom_to_xml (Sym {name, content}) = XML.Elem ("sym", attr "name" name, [XML.Text content])
+ fun atom_to_xml (Sym {name, content}) = XML.Elem (("sym", attr "name" name), [XML.Text content])
| atom_to_xml (Str content) = XML.Text content;
fun pgmlterm_to_xml (Atoms {kind, content}) =
- XML.Elem("atom", opt_attr "kind" kind, map atom_to_xml content)
+ XML.Elem(("atom", opt_attr "kind" kind), map atom_to_xml content)
| pgmlterm_to_xml (Box {orient, indent, content}) =
- XML.Elem("box",
+ XML.Elem(("box",
opt_attr_map pgmlorient_to_string "orient" orient @
- opt_attr_map int_to_pgstring "indent" indent,
+ opt_attr_map int_to_pgstring "indent" indent),
map pgmlterm_to_xml content)
| pgmlterm_to_xml (Break {mandatory, indent}) =
- XML.Elem("break",
+ XML.Elem(("break",
opt_attr_map bool_to_pgstring "mandatory" mandatory @
- opt_attr_map int_to_pgstring "indent" indent, [])
+ opt_attr_map int_to_pgstring "indent" indent), [])
| pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
- XML.Elem("subterm",
+ XML.Elem(("subterm",
opt_attr "kind" kind @
opt_attr "param" param @
opt_attr_map pgmlplace_to_string "place" place @
@@ -135,13 +135,13 @@
opt_attr_map pgmldec_to_string "decoration" decoration @
opt_attr_map pgmlaction_to_string "action" action @
opt_attr "pos" pos @
- opt_attr_map string_of_pgipurl "xref" xref,
+ opt_attr_map string_of_pgipurl "xref" xref),
map pgmlterm_to_xml content)
| pgmlterm_to_xml (Alt {kind, content}) =
- XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
+ XML.Elem(("alt", opt_attr "kind" kind), map pgmlterm_to_xml content)
- | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
+ | pgmlterm_to_xml (Embed xmls) = XML.Elem(("embed", []), xmls)
| pgmlterm_to_xml (Raw xml) = xml
@@ -152,9 +152,9 @@
content: pgmlterm list }
fun pgml_to_xml (Pgml {version,systemid,area,content}) =
- XML.Elem("pgml",
+ XML.Elem(("pgml",
opt_attr "version" version @
opt_attr "systemid" systemid @
- the_default [] (Option.map PgipTypes.attrs_of_displayarea area),
+ the_default [] (Option.map PgipTypes.attrs_of_displayarea area)),
map pgmlterm_to_xml content)
end
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Aug 07 21:03:06 2010 +0200
@@ -33,7 +33,7 @@
fun render_trees ts = fold render_tree ts
and render_tree (XML.Text s) = Buffer.add s
- | render_tree (XML.Elem (name, props, ts)) =
+ | render_tree (XML.Elem ((name, props), ts)) =
let
val (bg1, en1) =
if name <> Markup.promptN andalso print_mode_active test_markupN
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Aug 07 21:03:06 2010 +0200
@@ -105,7 +105,7 @@
in
-fun pgml_terms (XML.Elem (name, atts, body)) =
+fun pgml_terms (XML.Elem ((name, atts), body)) =
if member (op =) token_markups name then
let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
in [Pgml.Atoms {kind = SOME name, content = content}] end
@@ -132,7 +132,7 @@
val body = YXML.parse_body s;
val area =
(case body of
- [XML.Elem (name, _, _)] =>
+ [XML.Elem ((name, _), _)] =>
if name = Markup.stateN then PgipTypes.Display else default_area
| _ => default_area);
in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
@@ -283,8 +283,8 @@
fun thm_deps_message (thms, deps) =
let
- val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
- val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
+ val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]);
+ val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]);
in
issue_pgip (Metainforesponse
{attrs = [("infotype", "isabelle_theorem_dependencies")],
@@ -312,7 +312,7 @@
let val keywords = Keyword.dest_keywords ()
val commands = Keyword.dest_commands ()
fun keyword_elt kind keyword =
- XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
+ XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
in
(* Also, note we don't call init_outer_syntax here to add interface commands,
but they should never appear in scripts anyway so it shouldn't matter *)
@@ -647,8 +647,7 @@
fun idvalue strings =
issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
- text=[XML.Elem("pgml",[],
- maps YXML.parse_body strings)] })
+ text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
fun strings_of_thm (thy, name) =
map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
@@ -927,7 +926,7 @@
(pgip_refid := NONE;
pgip_refseq := NONE;
(case xml of
- XML.Elem ("pgip", attrs, pgips) =>
+ XML.Elem (("pgip", attrs), pgips) =>
(let
val class = PgipTypes.get_attr "class" attrs
val dest = PgipTypes.get_attr_opt "destid" attrs
--- a/src/Pure/Syntax/syntax.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat Aug 07 21:03:06 2010 +0200
@@ -460,8 +460,9 @@
fun read_token str =
let val (text, pos) =
(case YXML.parse str handle Fail msg => error msg of
- XML.Elem ("token", props, [XML.Text text]) => (text, Position.of_properties props)
- | XML.Elem ("token", props, []) => ("", Position.of_properties props)
+ (* FIXME avoid literal strings *)
+ XML.Elem (("token", props), [XML.Text text]) => (text, Position.of_properties props)
+ | XML.Elem (("token", props), []) => ("", Position.of_properties props)
| XML.Text text => (text, Position.none)
| _ => (str, Position.none))
in (Symbol_Pos.explode (text, pos), pos) end;
--- a/src/Pure/System/isabelle_process.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Sat Aug 07 21:03:06 2010 +0200
@@ -34,7 +34,7 @@
fun message _ _ _ "" = ()
| message out_stream ch props body =
let
- val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
+ val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), []));
val msg = Symbol.STX ^ chunk header ^ chunk body;
in TextIO.output (out_stream, msg) (*atomic output*) end;
--- a/src/Pure/Tools/xml_syntax.ML Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/Tools/xml_syntax.ML Sat Aug 07 21:03:06 2010 +0200
@@ -22,148 +22,150 @@
(**** XML output ****)
-fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
+fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
-fun xml_of_type (TVar ((s, i), S)) = XML.Elem ("TVar",
- ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
- map xml_of_class S)
+fun xml_of_type (TVar ((s, i), S)) =
+ XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+ map xml_of_class S)
| xml_of_type (TFree (s, S)) =
- XML.Elem ("TFree", [("name", s)], map xml_of_class S)
+ XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
| xml_of_type (Type (s, Ts)) =
- XML.Elem ("Type", [("name", s)], map xml_of_type Ts);
+ XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
fun xml_of_term (Bound i) =
- XML.Elem ("Bound", [("index", string_of_int i)], [])
+ XML.Elem (("Bound", [("index", string_of_int i)]), [])
| xml_of_term (Free (s, T)) =
- XML.Elem ("Free", [("name", s)], [xml_of_type T])
- | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
- ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
- [xml_of_type T])
+ XML.Elem (("Free", [("name", s)]), [xml_of_type T])
+ | xml_of_term (Var ((s, i), T)) =
+ XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+ [xml_of_type T])
| xml_of_term (Const (s, T)) =
- XML.Elem ("Const", [("name", s)], [xml_of_type T])
+ XML.Elem (("Const", [("name", s)]), [xml_of_type T])
| xml_of_term (t $ u) =
- XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
+ XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
| xml_of_term (Abs (s, T, t)) =
- XML.Elem ("Abs", [("vname", s)], [xml_of_type T, xml_of_term t]);
+ XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
fun xml_of_opttypes NONE = []
- | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_type Ts)];
+ | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
(* it can be looked up in the theorem database. Thus, it could be *)
(* omitted from the xml representation. *)
+(* FIXME not exhaustive *)
fun xml_of_proof (PBound i) =
- XML.Elem ("PBound", [("index", string_of_int i)], [])
+ XML.Elem (("PBound", [("index", string_of_int i)]), [])
| xml_of_proof (Abst (s, optT, prf)) =
- XML.Elem ("Abst", [("vname", s)],
- (case optT of NONE => [] | SOME T => [xml_of_type T]) @
- [xml_of_proof prf])
+ XML.Elem (("Abst", [("vname", s)]),
+ (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
| xml_of_proof (AbsP (s, optt, prf)) =
- XML.Elem ("AbsP", [("vname", s)],
- (case optt of NONE => [] | SOME t => [xml_of_term t]) @
- [xml_of_proof prf])
+ XML.Elem (("AbsP", [("vname", s)]),
+ (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
| xml_of_proof (prf % optt) =
- XML.Elem ("Appt", [],
- xml_of_proof prf ::
- (case optt of NONE => [] | SOME t => [xml_of_term t]))
+ XML.Elem (("Appt", []),
+ xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
| xml_of_proof (prf %% prf') =
- XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
- | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
+ XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
+ | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
| xml_of_proof (PThm (_, ((s, t, optTs), _))) =
- XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
+ XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
| xml_of_proof (PAxm (s, t, optTs)) =
- XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
+ XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
| xml_of_proof (Oracle (s, t, optTs)) =
- XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
+ XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
| xml_of_proof MinProof =
- XML.Elem ("MinProof", [], []);
+ XML.Elem (("MinProof", []), []);
+
(* useful for checking the output against a schema file *)
fun write_to_file path elname x =
File.write path
("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
- XML.string_of (XML.Elem (elname,
- [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
- ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")],
+ XML.string_of (XML.Elem ((elname,
+ [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
+ ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
[x])));
+
(**** XML input ****)
exception XML of string * XML.tree;
-fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
+fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
| class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
-fun index_of_string s tree idx = (case Int.fromString idx of
- NONE => raise XML (s ^ ": bad index", tree) | SOME i => i);
+fun index_of_string s tree idx =
+ (case Int.fromString idx of
+ NONE => raise XML (s ^ ": bad index", tree)
+ | SOME i => i);
-fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar
+fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
((case Properties.get atts "name" of
NONE => raise XML ("type_of_xml: name of TVar missing", tree)
| SOME name => name,
the_default 0 (Option.map (index_of_string "type_of_xml" tree)
(Properties.get atts "index"))),
map class_of_xml classes)
- | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) =
+ | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
TFree (s, map class_of_xml classes)
- | type_of_xml (XML.Elem ("Type", [("name", s)], types)) =
+ | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
Type (s, map type_of_xml types)
| type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
-fun term_of_xml (tree as XML.Elem ("Bound", [("index", idx)], [])) =
+fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
Bound (index_of_string "bad variable index" tree idx)
- | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) =
+ | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
Free (s, type_of_xml typ)
- | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var
+ | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
((case Properties.get atts "name" of
NONE => raise XML ("type_of_xml: name of Var missing", tree)
| SOME name => name,
the_default 0 (Option.map (index_of_string "term_of_xml" tree)
(Properties.get atts "index"))),
type_of_xml typ)
- | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) =
+ | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
Const (s, type_of_xml typ)
- | term_of_xml (XML.Elem ("App", [], [term, term'])) =
+ | term_of_xml (XML.Elem (("App", []), [term, term'])) =
term_of_xml term $ term_of_xml term'
- | term_of_xml (XML.Elem ("Abs", [("vname", s)], [typ, term])) =
+ | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
Abs (s, type_of_xml typ, term_of_xml term)
| term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
fun opttypes_of_xml [] = NONE
- | opttypes_of_xml [XML.Elem ("types", [], types)] =
+ | opttypes_of_xml [XML.Elem (("types", []), types)] =
SOME (map type_of_xml types)
| opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
-fun proof_of_xml (tree as XML.Elem ("PBound", [("index", idx)], [])) =
+fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
PBound (index_of_string "proof_of_xml" tree idx)
- | proof_of_xml (XML.Elem ("Abst", [("vname", s)], [proof])) =
+ | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
Abst (s, NONE, proof_of_xml proof)
- | proof_of_xml (XML.Elem ("Abst", [("vname", s)], [typ, proof])) =
+ | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
- | proof_of_xml (XML.Elem ("AbsP", [("vname", s)], [proof])) =
+ | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
AbsP (s, NONE, proof_of_xml proof)
- | proof_of_xml (XML.Elem ("AbsP", [("vname", s)], [term, proof])) =
+ | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
- | proof_of_xml (XML.Elem ("Appt", [], [proof])) =
+ | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
proof_of_xml proof % NONE
- | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) =
+ | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
proof_of_xml proof % SOME (term_of_xml term)
- | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) =
+ | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
proof_of_xml proof %% proof_of_xml proof'
- | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
+ | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
Hyp (term_of_xml term)
- | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
+ | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
(* FIXME? *)
PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
Future.value (Proofterm.approximate_proof_body MinProof)))
- | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
+ | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
- | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
+ | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
- | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof
+ | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
| proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
end;