simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
authorwenzelm
Sat Aug 07 21:03:06 2010 +0200 (2010-08-07 ago)
changeset 38228ada3ab6b9085
parent 38227 6bbb42843b6e
child 38229 61d0fe8b96ac
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
src/Pure/General/xml.ML
src/Pure/General/yxml.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/ProofGeneral/pgip_input.ML
src/Pure/ProofGeneral/pgip_markup.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/ProofGeneral/pgml.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Syntax/syntax.ML
src/Pure/System/isabelle_process.ML
src/Pure/Tools/xml_syntax.ML
     1.1 --- a/src/Pure/General/xml.ML	Sat Aug 07 19:52:14 2010 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Sat Aug 07 21:03:06 2010 +0200
     1.3 @@ -1,14 +1,14 @@
     1.4  (*  Title:      Pure/General/xml.ML
     1.5      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
     1.6  
     1.7 -Basic support for XML.
     1.8 +Simple XML tree values.
     1.9  *)
    1.10  
    1.11  signature XML =
    1.12  sig
    1.13    type attributes = Properties.T
    1.14    datatype tree =
    1.15 -      Elem of string * attributes * tree list
    1.16 +      Elem of Markup.T * tree list
    1.17      | Text of string
    1.18    val add_content: tree -> Buffer.T -> Buffer.T
    1.19    val header: string
    1.20 @@ -32,10 +32,10 @@
    1.21  type attributes = Properties.T;
    1.22  
    1.23  datatype tree =
    1.24 -    Elem of string * attributes * tree list
    1.25 +    Elem of Markup.T * tree list
    1.26    | Text of string;
    1.27  
    1.28 -fun add_content (Elem (_, _, ts)) = fold add_content ts
    1.29 +fun add_content (Elem (_, ts)) = fold add_content ts
    1.30    | add_content (Text s) = Buffer.add s;
    1.31  
    1.32  
    1.33 @@ -84,9 +84,9 @@
    1.34  
    1.35  fun buffer_of tree =
    1.36    let
    1.37 -    fun traverse (Elem (name, atts, [])) =
    1.38 +    fun traverse (Elem ((name, atts), [])) =
    1.39            Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
    1.40 -      | traverse (Elem (name, atts, ts)) =
    1.41 +      | traverse (Elem ((name, atts), ts)) =
    1.42            Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
    1.43            fold traverse ts #>
    1.44            Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    1.45 @@ -170,8 +170,7 @@
    1.46          (Scan.this_string "/>" >> ignored
    1.47           || $$ ">" |-- parse_content --|
    1.48              !! (err ("Expected </" ^ s ^ ">"))
    1.49 -              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >>
    1.50 -    (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
    1.51 +              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
    1.52  
    1.53  val parse_document =
    1.54    (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
     2.1 --- a/src/Pure/General/yxml.ML	Sat Aug 07 19:52:14 2010 +0200
     2.2 +++ b/src/Pure/General/yxml.ML	Sat Aug 07 21:03:06 2010 +0200
     2.3 @@ -64,7 +64,7 @@
     2.4      fun attrib (a, x) =
     2.5        Buffer.add Y #>
     2.6        Buffer.add a #> Buffer.add "=" #> Buffer.add x;
     2.7 -    fun tree (XML.Elem (name, atts, ts)) =
     2.8 +    fun tree (XML.Elem ((name, atts), ts)) =
     2.9            Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
    2.10            fold tree ts #>
    2.11            Buffer.add XYX
    2.12 @@ -104,7 +104,7 @@
    2.13    | push name atts pending = ((name, atts), []) :: pending;
    2.14  
    2.15  fun pop ((("", _), _) :: _) = err_unbalanced ""
    2.16 -  | pop (((name, atts), body) :: pending) = add (XML.Elem (name, atts, rev body)) pending;
    2.17 +  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
    2.18  
    2.19  
    2.20  (* parsing *)
     3.1 --- a/src/Pure/Isar/token.ML	Sat Aug 07 19:52:14 2010 +0200
     3.2 +++ b/src/Pure/Isar/token.ML	Sat Aug 07 21:03:06 2010 +0200
     3.3 @@ -181,7 +181,7 @@
     3.4  (* token content *)
     3.5  
     3.6  fun source_of (Token ((source, (pos, _)), _, _)) =
     3.7 -  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
     3.8 +  YXML.string_of (XML.Elem ((Markup.tokenN, Position.properties_of pos), [XML.Text source]));
     3.9  
    3.10  fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
    3.11  
     4.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Aug 07 19:52:14 2010 +0200
     4.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Aug 07 21:03:06 2010 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4        endLine = end_line, endPosition = end_offset} = loc;
     4.5      val loc_props =
     4.6        (case YXML.parse text of
     4.7 -        XML.Elem (e, atts, _) => if e = Markup.positionN then atts else []
     4.8 +        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
     4.9        | XML.Text s => Position.file_name s);
    4.10    in
    4.11      Position.value Markup.lineN line @
     5.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Sat Aug 07 19:52:14 2010 +0200
     5.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Sat Aug 07 21:03:06 2010 +0200
     5.3 @@ -62,7 +62,7 @@
     5.4      (* unofficial escape command for debugging *)
     5.5      | Quitpgip       of { }
     5.6  
     5.7 -    val input: string * XML.attributes * XML.tree list -> pgipinput option  (* raises PGIP *)
     5.8 +    val input: Markup.T * XML.tree list -> pgipinput option  (* raises PGIP *)
     5.9  end
    5.10  
    5.11  structure PgipInput : PGIPINPUT = 
    5.12 @@ -161,7 +161,7 @@
    5.13     Raise PGIP exception for invalid data.
    5.14     Return NONE for unknown/unhandled commands. 
    5.15  *)
    5.16 -fun input (elem, attrs, data) =
    5.17 +fun input ((elem, attrs), data) =
    5.18  SOME 
    5.19   (case elem of 
    5.20       "askpgip"        => Askpgip { }
     6.1 --- a/src/Pure/ProofGeneral/pgip_markup.ML	Sat Aug 07 19:52:14 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/pgip_markup.ML	Sat Aug 07 21:03:06 2010 +0200
     6.3 @@ -75,81 +75,81 @@
     6.4         case docelt of
     6.5  
     6.6             Openblock vs  =>
     6.7 -           XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
     6.8 -                                 opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
     6.9 -                                 opt_attr "metavarid" (#metavarid vs),
    6.10 +           XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
    6.11 +                                  opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
    6.12 +                                  opt_attr "metavarid" (#metavarid vs)),
    6.13                      [])
    6.14  
    6.15           | Closeblock _ =>
    6.16 -           XML.Elem("closeblock", [], [])
    6.17 +           XML.Elem(("closeblock", []), [])
    6.18  
    6.19           | Opentheory vs  =>
    6.20 -           XML.Elem("opentheory",
    6.21 +           XML.Elem(("opentheory",
    6.22                      opt_attr "thyname" (#thyname vs) @
    6.23                      opt_attr "parentnames"
    6.24                               (case (#parentnames vs)
    6.25                                 of [] => NONE
    6.26 -                                | ps => SOME (space_implode ";" ps)),
    6.27 +                                | ps => SOME (space_implode ";" ps))),
    6.28                      [XML.Text (#text vs)])
    6.29  
    6.30           | Theoryitem vs =>
    6.31 -           XML.Elem("theoryitem",
    6.32 +           XML.Elem(("theoryitem",
    6.33                      opt_attr "name" (#name vs) @
    6.34 -                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
    6.35 +                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs)),
    6.36                      [XML.Text (#text vs)])
    6.37  
    6.38           | Closetheory vs =>
    6.39 -           XML.Elem("closetheory", [], [XML.Text (#text vs)])
    6.40 +           XML.Elem(("closetheory", []), [XML.Text (#text vs)])
    6.41  
    6.42           | Opengoal vs =>
    6.43 -           XML.Elem("opengoal",
    6.44 -                    opt_attr "thmname" (#thmname vs),
    6.45 +           XML.Elem(("opengoal",
    6.46 +                    opt_attr "thmname" (#thmname vs)),
    6.47                      [XML.Text (#text vs)])
    6.48  
    6.49           | Proofstep vs =>
    6.50 -           XML.Elem("proofstep", [], [XML.Text (#text vs)])
    6.51 +           XML.Elem(("proofstep", []), [XML.Text (#text vs)])
    6.52  
    6.53           | Closegoal vs =>
    6.54 -           XML.Elem("closegoal", [], [XML.Text (#text vs)])
    6.55 +           XML.Elem(("closegoal", []), [XML.Text (#text vs)])
    6.56  
    6.57           | Giveupgoal vs =>
    6.58 -           XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
    6.59 +           XML.Elem(("giveupgoal", []), [XML.Text (#text vs)])
    6.60  
    6.61           | Postponegoal vs =>
    6.62 -           XML.Elem("postponegoal", [], [XML.Text (#text vs)])
    6.63 +           XML.Elem(("postponegoal", []), [XML.Text (#text vs)])
    6.64  
    6.65           | Comment vs =>
    6.66 -           XML.Elem("comment", [], [XML.Text (#text vs)])
    6.67 +           XML.Elem(("comment", []), [XML.Text (#text vs)])
    6.68  
    6.69           | Whitespace vs =>
    6.70 -           XML.Elem("whitespace", [], [XML.Text (#text vs)])
    6.71 +           XML.Elem(("whitespace", []), [XML.Text (#text vs)])
    6.72  
    6.73           | Doccomment vs =>
    6.74 -           XML.Elem("doccomment", [], [XML.Text (#text vs)])
    6.75 +           XML.Elem(("doccomment", []), [XML.Text (#text vs)])
    6.76  
    6.77           | Spuriouscmd vs =>
    6.78 -           XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
    6.79 +           XML.Elem(("spuriouscmd", []), [XML.Text (#text vs)])
    6.80  
    6.81           | Badcmd vs =>
    6.82 -           XML.Elem("badcmd", [], [XML.Text (#text vs)])
    6.83 +           XML.Elem(("badcmd", []), [XML.Text (#text vs)])
    6.84  
    6.85           | Unparseable vs =>
    6.86 -           XML.Elem("unparseable", [], [XML.Text (#text vs)])
    6.87 +           XML.Elem(("unparseable", []), [XML.Text (#text vs)])
    6.88  
    6.89           | Metainfo vs =>
    6.90 -           XML.Elem("metainfo", opt_attr "name" (#name vs),
    6.91 +           XML.Elem(("metainfo", opt_attr "name" (#name vs)),
    6.92                      [XML.Text (#text vs)])
    6.93  
    6.94           | Litcomment vs =>
    6.95 -           XML.Elem("litcomment", opt_attr "format" (#format vs),
    6.96 +           XML.Elem(("litcomment", opt_attr "format" (#format vs)),
    6.97                     #content vs)
    6.98  
    6.99           | Showcode vs =>
   6.100 -           XML.Elem("showcode",
   6.101 -                    attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
   6.102 +           XML.Elem(("showcode",
   6.103 +                    attr "show" (PgipTypes.bool_to_pgstring (#show vs))), [])
   6.104  
   6.105           | Setformat vs =>
   6.106 -           XML.Elem("setformat", attr "format" (#format vs), [])
   6.107 +           XML.Elem(("setformat", attr "format" (#format vs)), [])
   6.108  
   6.109     val output_doc = map xml_of
   6.110  
     7.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Sat Aug 07 19:52:14 2010 +0200
     7.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Sat Aug 07 21:03:06 2010 +0200
     7.3 @@ -117,9 +117,7 @@
     7.4      let 
     7.5          val content = #content vs
     7.6      in
     7.7 -        XML.Elem ("normalresponse", 
     7.8 -                  [],
     7.9 -                  content)
    7.10 +        XML.Elem (("normalresponse", []), content)
    7.11      end
    7.12  
    7.13  fun errorresponse (Errorresponse vs) =
    7.14 @@ -128,9 +126,9 @@
    7.15          val location = #location vs
    7.16          val content = #content vs
    7.17      in
    7.18 -        XML.Elem ("errorresponse",
    7.19 +        XML.Elem (("errorresponse",
    7.20                   attrs_of_fatality fatality @
    7.21 -                 these (Option.map attrs_of_location location),
    7.22 +                 these (Option.map attrs_of_location location)),
    7.23                   content)
    7.24      end
    7.25  
    7.26 @@ -139,9 +137,9 @@
    7.27          val url = #url vs
    7.28          val completed = #completed vs
    7.29      in
    7.30 -        XML.Elem ("informfileloaded", 
    7.31 +        XML.Elem (("informfileloaded", 
    7.32                    attrs_of_pgipurl url @ 
    7.33 -                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
    7.34 +                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
    7.35                    [])
    7.36      end
    7.37  
    7.38 @@ -150,9 +148,9 @@
    7.39          val url = #url vs
    7.40          val completed = #completed vs
    7.41      in
    7.42 -        XML.Elem ("informfileoutdated", 
    7.43 +        XML.Elem (("informfileoutdated", 
    7.44                    attrs_of_pgipurl url @ 
    7.45 -                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
    7.46 +                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
    7.47                    [])
    7.48      end
    7.49  
    7.50 @@ -161,9 +159,9 @@
    7.51          val url = #url vs
    7.52          val completed = #completed vs
    7.53      in
    7.54 -        XML.Elem ("informfileretracted", 
    7.55 +        XML.Elem (("informfileretracted", 
    7.56                    attrs_of_pgipurl url @ 
    7.57 -                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
    7.58 +                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
    7.59                    [])
    7.60      end
    7.61  
    7.62 @@ -172,14 +170,14 @@
    7.63          val attrs = #attrs vs
    7.64          val content = #content vs
    7.65      in
    7.66 -        XML.Elem ("metainforesponse", attrs, content)
    7.67 +        XML.Elem (("metainforesponse", attrs), content)
    7.68      end
    7.69  
    7.70  fun lexicalstructure (Lexicalstructure vs) =
    7.71      let
    7.72          val content = #content vs
    7.73      in
    7.74 -        XML.Elem ("lexicalstructure", [], content)
    7.75 +        XML.Elem (("lexicalstructure", []), content)
    7.76      end
    7.77  
    7.78  fun proverinfo (Proverinfo vs) =
    7.79 @@ -191,13 +189,13 @@
    7.80          val url = #url vs
    7.81          val filenameextns = #filenameextns vs
    7.82      in 
    7.83 -        XML.Elem ("proverinfo",
    7.84 +        XML.Elem (("proverinfo",
    7.85                   [("name", name),
    7.86                    ("version", version),
    7.87                    ("instance", instance), 
    7.88                    ("descr", descr),
    7.89                    ("url", Url.implode url),
    7.90 -                  ("filenameextns", filenameextns)],
    7.91 +                  ("filenameextns", filenameextns)]),
    7.92                   [])
    7.93      end
    7.94  
    7.95 @@ -205,7 +203,7 @@
    7.96      let
    7.97          val idtables = #idtables vs
    7.98      in
    7.99 -        XML.Elem ("setids",[],map idtable_to_xml idtables)
   7.100 +        XML.Elem (("setids", []), map idtable_to_xml idtables)
   7.101      end
   7.102  
   7.103  fun setrefs (Setrefs vs) =
   7.104 @@ -216,13 +214,13 @@
   7.105          val name = #name vs
   7.106          val idtables = #idtables vs
   7.107          val fileurls = #fileurls vs
   7.108 -        fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
   7.109 +        fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
   7.110      in
   7.111 -        XML.Elem ("setrefs",
   7.112 +        XML.Elem (("setrefs",
   7.113                    (the_default [] (Option.map attrs_of_pgipurl url)) @ 
   7.114                    (the_default [] (Option.map attrs_of_objtype objtype)) @
   7.115                    (opt_attr "thyname" thyname) @
   7.116 -                  (opt_attr "name" name),
   7.117 +                  (opt_attr "name" name)),
   7.118                    (map idtable_to_xml idtables) @ 
   7.119                    (map fileurl_to_xml fileurls))
   7.120      end
   7.121 @@ -231,14 +229,14 @@
   7.122      let
   7.123          val idtables = #idtables vs
   7.124      in
   7.125 -        XML.Elem ("addids",[],map idtable_to_xml idtables)
   7.126 +        XML.Elem (("addids", []), map idtable_to_xml idtables)
   7.127      end
   7.128  
   7.129  fun delids (Delids vs) =
   7.130      let
   7.131          val idtables = #idtables vs
   7.132      in
   7.133 -        XML.Elem ("delids",[],map idtable_to_xml idtables)
   7.134 +        XML.Elem (("delids", []), map idtable_to_xml idtables)
   7.135      end
   7.136  
   7.137  fun hasprefs (Hasprefs vs) =
   7.138 @@ -246,7 +244,7 @@
   7.139        val prefcategory = #prefcategory vs
   7.140        val prefs = #prefs vs
   7.141    in 
   7.142 -      XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
   7.143 +      XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
   7.144    end
   7.145  
   7.146  fun prefval (Prefval vs) =
   7.147 @@ -254,7 +252,7 @@
   7.148          val name = #name vs
   7.149          val value = #value vs
   7.150      in
   7.151 -        XML.Elem("prefval", attr "name" name, [XML.Text value])
   7.152 +        XML.Elem (("prefval", attr "name" name), [XML.Text value])
   7.153      end 
   7.154  
   7.155  fun idvalue (Idvalue vs) =
   7.156 @@ -264,10 +262,10 @@
   7.157          val name = #name vs
   7.158          val text = #text vs
   7.159      in
   7.160 -        XML.Elem("idvalue", 
   7.161 +        XML.Elem (("idvalue", 
   7.162                   objtype_attrs @
   7.163                   (opt_attr "thyname" thyname) @
   7.164 -                 (attr "name" name),
   7.165 +                 attr "name" name),
   7.166                   text)
   7.167      end
   7.168  
   7.169 @@ -278,7 +276,7 @@
   7.170        val theorem = #theorem vs
   7.171        val proofpos = #proofpos vs
   7.172  
   7.173 -      fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])]
   7.174 +      fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
   7.175  
   7.176        val guisefile = elto "guisefile" attrs_of_pgipurl file
   7.177        val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
   7.178 @@ -286,7 +284,7 @@
   7.179                              (fn thm=>(attr "thmname" thm) @
   7.180                                       (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
   7.181    in 
   7.182 -      XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
   7.183 +      XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
   7.184    end
   7.185  
   7.186  fun parseresult (Parseresult vs) =
   7.187 @@ -296,7 +294,7 @@
   7.188          val errs = #errs vs
   7.189          val xmldoc = PgipMarkup.output_doc doc
   7.190      in 
   7.191 -        XML.Elem("parseresult", attrs, errs @ xmldoc)
   7.192 +        XML.Elem (("parseresult", attrs), errs @ xmldoc)
   7.193      end
   7.194  
   7.195  fun acceptedpgipelems (Usespgip vs) = 
   7.196 @@ -305,11 +303,10 @@
   7.197          fun async_attrs b = if b then attr "async" "true" else []
   7.198          fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
   7.199          fun singlepgipelem (e,async,attrs) = 
   7.200 -            XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e])
   7.201 +            XML.Elem (("pgipelem", async_attrs async @ attrs_attrs attrs), [XML.Text e])
   7.202                                                        
   7.203      in
   7.204 -        XML.Elem ("acceptedpgipelems", [],
   7.205 -                 map singlepgipelem pgipelems)
   7.206 +        XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
   7.207      end
   7.208  
   7.209  fun usespgip (Usespgip vs) =
   7.210 @@ -317,14 +314,14 @@
   7.211          val version = #version vs
   7.212          val acceptedelems = acceptedpgipelems (Usespgip vs)
   7.213      in 
   7.214 -        XML.Elem("usespgip", attr "version" version, [acceptedelems])
   7.215 +        XML.Elem (("usespgip", attr "version" version), [acceptedelems])
   7.216      end
   7.217  
   7.218  fun usespgml (Usespgml vs) =
   7.219      let
   7.220          val version = #version vs
   7.221      in 
   7.222 -        XML.Elem("usespgml", attr "version" version, [])
   7.223 +        XML.Elem (("usespgml", attr "version" version), [])
   7.224      end
   7.225  
   7.226  fun pgip (Pgip vs) =
   7.227 @@ -338,18 +335,18 @@
   7.228          val refseq = #refseq vs
   7.229          val content = #content vs
   7.230      in
   7.231 -        XML.Elem("pgip",
   7.232 +        XML.Elem(("pgip",
   7.233                   opt_attr "tag" tag @
   7.234                   attr "id" id @
   7.235                   opt_attr "destid" destid @
   7.236                   attr "class" class @
   7.237                   opt_attr "refid" refid @
   7.238                   opt_attr_map string_of_int "refseq" refseq @
   7.239 -                 attr "seq" (string_of_int seq),
   7.240 +                 attr "seq" (string_of_int seq)),
   7.241                   content)
   7.242      end
   7.243  
   7.244 -fun ready (Ready _) = XML.Elem("ready",[],[])
   7.245 +fun ready (Ready _) = XML.Elem (("ready", []), [])
   7.246  
   7.247  
   7.248  fun output pgipoutput = case pgipoutput of
     8.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Sat Aug 07 19:52:14 2010 +0200
     8.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Sat Aug 07 21:03:06 2010 +0200
     8.3 @@ -168,11 +168,9 @@
     8.4      let 
     8.5          val objtype_attrs = attrs_of_objtype objtype
     8.6          val context_attrs = opt_attr "context" context
     8.7 -        val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
     8.8 +        val ids_content = map (fn x => XML.Elem(("identifier", []), [XML.Text x])) ids
     8.9      in 
    8.10 -        XML.Elem ("idtable",
    8.11 -                  objtype_attrs @ context_attrs,
    8.12 -                  ids_content)
    8.13 +        XML.Elem (("idtable", objtype_attrs @ context_attrs), ids_content)
    8.14      end
    8.15  
    8.16  
    8.17 @@ -282,7 +280,7 @@
    8.18                            Pgipchoice ds => map destpgipdtype ds
    8.19                          | _ => []
    8.20      in 
    8.21 -        XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
    8.22 +        XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs)
    8.23      end
    8.24  
    8.25  val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
    8.26 @@ -424,10 +422,10 @@
    8.27                      pgiptype: pgiptype }
    8.28  
    8.29  fun haspref ({ name, descr, default, pgiptype}:preference) = 
    8.30 -    XML.Elem ("haspref",
    8.31 +    XML.Elem (("haspref",
    8.32                attr "name" name @
    8.33                opt_attr "descr" descr @
    8.34 -              opt_attr "default" default,
    8.35 +              opt_attr "default" default),
    8.36                [pgiptype_to_xml pgiptype])
    8.37  
    8.38  end
     9.1 --- a/src/Pure/ProofGeneral/pgml.ML	Sat Aug 07 19:52:14 2010 +0200
     9.2 +++ b/src/Pure/ProofGeneral/pgml.ML	Sat Aug 07 21:03:06 2010 +0200
     9.3 @@ -109,25 +109,25 @@
     9.4  
     9.5      (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
     9.6         would be better not to *)  (* FIXME !??? *)
     9.7 -    fun atom_to_xml (Sym {name, content}) = XML.Elem ("sym", attr "name" name, [XML.Text content])
     9.8 +    fun atom_to_xml (Sym {name, content}) = XML.Elem (("sym", attr "name" name), [XML.Text content])
     9.9        | atom_to_xml (Str content) = XML.Text content;
    9.10  
    9.11      fun pgmlterm_to_xml (Atoms {kind, content}) =
    9.12 -        XML.Elem("atom", opt_attr "kind" kind, map atom_to_xml content)
    9.13 +        XML.Elem(("atom", opt_attr "kind" kind), map atom_to_xml content)
    9.14  
    9.15        | pgmlterm_to_xml (Box {orient, indent, content}) =
    9.16 -        XML.Elem("box",
    9.17 +        XML.Elem(("box",
    9.18                   opt_attr_map pgmlorient_to_string "orient" orient @
    9.19 -                 opt_attr_map int_to_pgstring "indent" indent,
    9.20 +                 opt_attr_map int_to_pgstring "indent" indent),
    9.21                   map pgmlterm_to_xml content)
    9.22  
    9.23        | pgmlterm_to_xml (Break {mandatory, indent}) =
    9.24 -        XML.Elem("break",
    9.25 +        XML.Elem(("break",
    9.26                   opt_attr_map bool_to_pgstring "mandatory" mandatory @
    9.27 -                 opt_attr_map int_to_pgstring "indent" indent, [])
    9.28 +                 opt_attr_map int_to_pgstring "indent" indent), [])
    9.29  
    9.30        | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
    9.31 -        XML.Elem("subterm",
    9.32 +        XML.Elem(("subterm",
    9.33                   opt_attr "kind" kind @
    9.34                   opt_attr "param" param @
    9.35                   opt_attr_map pgmlplace_to_string "place" place @
    9.36 @@ -135,13 +135,13 @@
    9.37                   opt_attr_map pgmldec_to_string "decoration" decoration @
    9.38                   opt_attr_map pgmlaction_to_string "action" action @
    9.39                   opt_attr "pos" pos @
    9.40 -                 opt_attr_map string_of_pgipurl "xref" xref,
    9.41 +                 opt_attr_map string_of_pgipurl "xref" xref),
    9.42                   map pgmlterm_to_xml content)
    9.43  
    9.44        | pgmlterm_to_xml (Alt {kind, content}) =
    9.45 -        XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
    9.46 +        XML.Elem(("alt", opt_attr "kind" kind), map pgmlterm_to_xml content)
    9.47  
    9.48 -      | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
    9.49 +      | pgmlterm_to_xml (Embed xmls) = XML.Elem(("embed", []), xmls)
    9.50  
    9.51        | pgmlterm_to_xml (Raw xml) = xml
    9.52  
    9.53 @@ -152,9 +152,9 @@
    9.54                         content: pgmlterm list }
    9.55  
    9.56      fun pgml_to_xml (Pgml {version,systemid,area,content}) =
    9.57 -        XML.Elem("pgml",
    9.58 +        XML.Elem(("pgml",
    9.59                   opt_attr "version" version @
    9.60                   opt_attr "systemid" systemid @
    9.61 -                 the_default [] (Option.map PgipTypes.attrs_of_displayarea area),
    9.62 +                 the_default [] (Option.map PgipTypes.attrs_of_displayarea area)),
    9.63                   map pgmlterm_to_xml content)
    9.64  end
    10.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Aug 07 19:52:14 2010 +0200
    10.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Aug 07 21:03:06 2010 +0200
    10.3 @@ -33,7 +33,7 @@
    10.4  
    10.5  fun render_trees ts = fold render_tree ts
    10.6  and render_tree (XML.Text s) = Buffer.add s
    10.7 -  | render_tree (XML.Elem (name, props, ts)) =
    10.8 +  | render_tree (XML.Elem ((name, props), ts)) =
    10.9        let
   10.10          val (bg1, en1) =
   10.11            if name <> Markup.promptN andalso print_mode_active test_markupN
    11.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Aug 07 19:52:14 2010 +0200
    11.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Aug 07 21:03:06 2010 +0200
    11.3 @@ -105,7 +105,7 @@
    11.4  
    11.5  in
    11.6  
    11.7 -fun pgml_terms (XML.Elem (name, atts, body)) =
    11.8 +fun pgml_terms (XML.Elem ((name, atts), body)) =
    11.9        if member (op =) token_markups name then
   11.10          let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
   11.11          in [Pgml.Atoms {kind = SOME name, content = content}] end
   11.12 @@ -132,7 +132,7 @@
   11.13      val body = YXML.parse_body s;
   11.14      val area =
   11.15        (case body of
   11.16 -        [XML.Elem (name, _, _)] =>
   11.17 +        [XML.Elem ((name, _), _)] =>
   11.18            if name = Markup.stateN then PgipTypes.Display else default_area
   11.19        | _ => default_area);
   11.20    in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
   11.21 @@ -283,8 +283,8 @@
   11.22  
   11.23  fun thm_deps_message (thms, deps) =
   11.24    let
   11.25 -    val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
   11.26 -    val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
   11.27 +    val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]);
   11.28 +    val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]);
   11.29    in
   11.30      issue_pgip (Metainforesponse
   11.31        {attrs = [("infotype", "isabelle_theorem_dependencies")],
   11.32 @@ -312,7 +312,7 @@
   11.33      let val keywords = Keyword.dest_keywords ()
   11.34          val commands = Keyword.dest_commands ()
   11.35          fun keyword_elt kind keyword =
   11.36 -            XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
   11.37 +            XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
   11.38          in
   11.39              (* Also, note we don't call init_outer_syntax here to add interface commands,
   11.40              but they should never appear in scripts anyway so it shouldn't matter *)
   11.41 @@ -647,8 +647,7 @@
   11.42  
   11.43          fun idvalue strings =
   11.44              issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
   11.45 -                                  text=[XML.Elem("pgml",[],
   11.46 -                                                 maps YXML.parse_body strings)] })
   11.47 +                                  text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
   11.48  
   11.49          fun strings_of_thm (thy, name) =
   11.50            map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
   11.51 @@ -927,7 +926,7 @@
   11.52      (pgip_refid := NONE;
   11.53       pgip_refseq := NONE;
   11.54       (case xml of
   11.55 -          XML.Elem ("pgip", attrs, pgips) =>
   11.56 +          XML.Elem (("pgip", attrs), pgips) =>
   11.57            (let
   11.58                 val class = PgipTypes.get_attr "class" attrs
   11.59                 val dest  = PgipTypes.get_attr_opt "destid" attrs
    12.1 --- a/src/Pure/Syntax/syntax.ML	Sat Aug 07 19:52:14 2010 +0200
    12.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Aug 07 21:03:06 2010 +0200
    12.3 @@ -460,8 +460,9 @@
    12.4  fun read_token str =
    12.5    let val (text, pos) =
    12.6      (case YXML.parse str handle Fail msg => error msg of
    12.7 -      XML.Elem ("token", props, [XML.Text text]) => (text, Position.of_properties props)
    12.8 -    | XML.Elem ("token", props, []) => ("", Position.of_properties props)
    12.9 +    (* FIXME avoid literal strings *)
   12.10 +      XML.Elem (("token", props), [XML.Text text]) => (text, Position.of_properties props)
   12.11 +    | XML.Elem (("token", props), []) => ("", Position.of_properties props)
   12.12      | XML.Text text => (text, Position.none)
   12.13      | _ => (str, Position.none))
   12.14    in (Symbol_Pos.explode (text, pos), pos) end;
    13.1 --- a/src/Pure/System/isabelle_process.ML	Sat Aug 07 19:52:14 2010 +0200
    13.2 +++ b/src/Pure/System/isabelle_process.ML	Sat Aug 07 21:03:06 2010 +0200
    13.3 @@ -34,7 +34,7 @@
    13.4  fun message _ _ _ "" = ()
    13.5    | message out_stream ch props body =
    13.6        let
    13.7 -        val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
    13.8 +        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), []));
    13.9          val msg = Symbol.STX ^ chunk header ^ chunk body;
   13.10        in TextIO.output (out_stream, msg) (*atomic output*) end;
   13.11  
    14.1 --- a/src/Pure/Tools/xml_syntax.ML	Sat Aug 07 19:52:14 2010 +0200
    14.2 +++ b/src/Pure/Tools/xml_syntax.ML	Sat Aug 07 21:03:06 2010 +0200
    14.3 @@ -22,148 +22,150 @@
    14.4  
    14.5  (**** XML output ****)
    14.6  
    14.7 -fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
    14.8 +fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
    14.9  
   14.10 -fun xml_of_type (TVar ((s, i), S)) = XML.Elem ("TVar",
   14.11 -      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
   14.12 -      map xml_of_class S)
   14.13 +fun xml_of_type (TVar ((s, i), S)) =
   14.14 +      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
   14.15 +        map xml_of_class S)
   14.16    | xml_of_type (TFree (s, S)) =
   14.17 -      XML.Elem ("TFree", [("name", s)], map xml_of_class S)
   14.18 +      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
   14.19    | xml_of_type (Type (s, Ts)) =
   14.20 -      XML.Elem ("Type", [("name", s)], map xml_of_type Ts);
   14.21 +      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
   14.22  
   14.23  fun xml_of_term (Bound i) =
   14.24 -      XML.Elem ("Bound", [("index", string_of_int i)], [])
   14.25 +      XML.Elem (("Bound", [("index", string_of_int i)]), [])
   14.26    | xml_of_term (Free (s, T)) =
   14.27 -      XML.Elem ("Free", [("name", s)], [xml_of_type T])
   14.28 -  | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
   14.29 -      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
   14.30 -      [xml_of_type T])
   14.31 +      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
   14.32 +  | xml_of_term (Var ((s, i), T)) =
   14.33 +      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
   14.34 +        [xml_of_type T])
   14.35    | xml_of_term (Const (s, T)) =
   14.36 -      XML.Elem ("Const", [("name", s)], [xml_of_type T])
   14.37 +      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
   14.38    | xml_of_term (t $ u) =
   14.39 -      XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
   14.40 +      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
   14.41    | xml_of_term (Abs (s, T, t)) =
   14.42 -      XML.Elem ("Abs", [("vname", s)], [xml_of_type T, xml_of_term t]);
   14.43 +      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
   14.44  
   14.45  fun xml_of_opttypes NONE = []
   14.46 -  | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_type Ts)];
   14.47 +  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
   14.48  
   14.49  (* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
   14.50  (* it can be looked up in the theorem database. Thus, it could be      *)
   14.51  (* omitted from the xml representation.                                *)
   14.52  
   14.53 +(* FIXME not exhaustive *)
   14.54  fun xml_of_proof (PBound i) =
   14.55 -      XML.Elem ("PBound", [("index", string_of_int i)], [])
   14.56 +      XML.Elem (("PBound", [("index", string_of_int i)]), [])
   14.57    | xml_of_proof (Abst (s, optT, prf)) =
   14.58 -      XML.Elem ("Abst", [("vname", s)],
   14.59 -        (case optT of NONE => [] | SOME T => [xml_of_type T]) @
   14.60 -        [xml_of_proof prf])
   14.61 +      XML.Elem (("Abst", [("vname", s)]),
   14.62 +        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
   14.63    | xml_of_proof (AbsP (s, optt, prf)) =
   14.64 -      XML.Elem ("AbsP", [("vname", s)],
   14.65 -        (case optt of NONE => [] | SOME t => [xml_of_term t]) @
   14.66 -        [xml_of_proof prf])
   14.67 +      XML.Elem (("AbsP", [("vname", s)]),
   14.68 +        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
   14.69    | xml_of_proof (prf % optt) =
   14.70 -      XML.Elem ("Appt", [],
   14.71 -        xml_of_proof prf ::
   14.72 -        (case optt of NONE => [] | SOME t => [xml_of_term t]))
   14.73 +      XML.Elem (("Appt", []),
   14.74 +        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
   14.75    | xml_of_proof (prf %% prf') =
   14.76 -      XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
   14.77 -  | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
   14.78 +      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
   14.79 +  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
   14.80    | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
   14.81 -      XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   14.82 +      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   14.83    | xml_of_proof (PAxm (s, t, optTs)) =
   14.84 -      XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   14.85 +      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   14.86    | xml_of_proof (Oracle (s, t, optTs)) =
   14.87 -      XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   14.88 +      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   14.89    | xml_of_proof MinProof =
   14.90 -      XML.Elem ("MinProof", [], []);
   14.91 +      XML.Elem (("MinProof", []), []);
   14.92 +
   14.93  
   14.94  (* useful for checking the output against a schema file *)
   14.95  
   14.96  fun write_to_file path elname x =
   14.97    File.write path
   14.98      ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
   14.99 -     XML.string_of (XML.Elem (elname,
  14.100 -       [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
  14.101 -        ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")],
  14.102 +     XML.string_of (XML.Elem ((elname,
  14.103 +         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
  14.104 +          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
  14.105         [x])));
  14.106  
  14.107  
  14.108 +
  14.109  (**** XML input ****)
  14.110  
  14.111  exception XML of string * XML.tree;
  14.112  
  14.113 -fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
  14.114 +fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
  14.115    | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
  14.116  
  14.117 -fun index_of_string s tree idx = (case Int.fromString idx of
  14.118 -  NONE => raise XML (s ^ ": bad index", tree) | SOME i => i);
  14.119 +fun index_of_string s tree idx =
  14.120 +  (case Int.fromString idx of
  14.121 +    NONE => raise XML (s ^ ": bad index", tree)
  14.122 +  | SOME i => i);
  14.123  
  14.124 -fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar
  14.125 +fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
  14.126        ((case Properties.get atts "name" of
  14.127            NONE => raise XML ("type_of_xml: name of TVar missing", tree)
  14.128          | SOME name => name,
  14.129          the_default 0 (Option.map (index_of_string "type_of_xml" tree)
  14.130            (Properties.get atts "index"))),
  14.131         map class_of_xml classes)
  14.132 -  | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) =
  14.133 +  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
  14.134        TFree (s, map class_of_xml classes)
  14.135 -  | type_of_xml (XML.Elem ("Type", [("name", s)], types)) =
  14.136 +  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
  14.137        Type (s, map type_of_xml types)
  14.138    | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
  14.139  
  14.140 -fun term_of_xml (tree as XML.Elem ("Bound", [("index", idx)], [])) =
  14.141 +fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
  14.142        Bound (index_of_string "bad variable index" tree idx)
  14.143 -  | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) =
  14.144 +  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
  14.145        Free (s, type_of_xml typ)
  14.146 -  | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var
  14.147 +  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
  14.148        ((case Properties.get atts "name" of
  14.149            NONE => raise XML ("type_of_xml: name of Var missing", tree)
  14.150          | SOME name => name,
  14.151          the_default 0 (Option.map (index_of_string "term_of_xml" tree)
  14.152            (Properties.get atts "index"))),
  14.153         type_of_xml typ)
  14.154 -  | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) =
  14.155 +  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
  14.156        Const (s, type_of_xml typ)
  14.157 -  | term_of_xml (XML.Elem ("App", [], [term, term'])) =
  14.158 +  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
  14.159        term_of_xml term $ term_of_xml term'
  14.160 -  | term_of_xml (XML.Elem ("Abs", [("vname", s)], [typ, term])) =
  14.161 +  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
  14.162        Abs (s, type_of_xml typ, term_of_xml term)
  14.163    | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
  14.164  
  14.165  fun opttypes_of_xml [] = NONE
  14.166 -  | opttypes_of_xml [XML.Elem ("types", [], types)] =
  14.167 +  | opttypes_of_xml [XML.Elem (("types", []), types)] =
  14.168        SOME (map type_of_xml types)
  14.169    | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
  14.170  
  14.171 -fun proof_of_xml (tree as XML.Elem ("PBound", [("index", idx)], [])) =
  14.172 +fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
  14.173        PBound (index_of_string "proof_of_xml" tree idx)
  14.174 -  | proof_of_xml (XML.Elem ("Abst", [("vname", s)], [proof])) =
  14.175 +  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
  14.176        Abst (s, NONE, proof_of_xml proof)
  14.177 -  | proof_of_xml (XML.Elem ("Abst", [("vname", s)], [typ, proof])) =
  14.178 +  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
  14.179        Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
  14.180 -  | proof_of_xml (XML.Elem ("AbsP", [("vname", s)], [proof])) =
  14.181 +  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
  14.182        AbsP (s, NONE, proof_of_xml proof)
  14.183 -  | proof_of_xml (XML.Elem ("AbsP", [("vname", s)], [term, proof])) =
  14.184 +  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
  14.185        AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
  14.186 -  | proof_of_xml (XML.Elem ("Appt", [], [proof])) =
  14.187 +  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
  14.188        proof_of_xml proof % NONE
  14.189 -  | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) =
  14.190 +  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
  14.191        proof_of_xml proof % SOME (term_of_xml term)
  14.192 -  | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) =
  14.193 +  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
  14.194        proof_of_xml proof %% proof_of_xml proof'
  14.195 -  | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
  14.196 +  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
  14.197        Hyp (term_of_xml term)
  14.198 -  | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
  14.199 +  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
  14.200        (* FIXME? *)
  14.201        PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
  14.202          Future.value (Proofterm.approximate_proof_body MinProof)))
  14.203 -  | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
  14.204 +  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
  14.205        PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
  14.206 -  | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
  14.207 +  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
  14.208        Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
  14.209 -  | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof
  14.210 +  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
  14.211    | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
  14.212  
  14.213  end;