# HG changeset patch
# User wenzelm
# Date 1281207786 -7200
# Node ID ada3ab6b9085437a95530a64e7f28672565ff2fa
# Parent  6bbb42843b6ecde79d908b89b13f8c6a07eeeb29
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;

diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/General/xml.ML
--- 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)
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/General/yxml.ML
--- 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 *)
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/Isar/token.ML
--- 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);
 
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- 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 @
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/pgip_input.ML
--- 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 { }
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/pgip_markup.ML
--- 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
 
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/pgip_output.ML
--- 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
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/pgip_types.ML
--- 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
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/pgml.ML
--- 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
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/Syntax/syntax.ML
--- 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;
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/System/isabelle_process.ML
--- 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;
 
diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/Tools/xml_syntax.ML
--- 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;