diff --git a/src/Pure/PIDE/xml.ML b/src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML
+++ b/src/Pure/PIDE/xml.ML
@@ -1,421 +1,423 @@
 (*  Title:      Pure/PIDE/xml.ML
     Author:     David Aspinall
     Author:     Stefan Berghofer
     Author:     Makarius
 
 Untyped XML trees and representation of ML values.
 *)
 
 signature XML_DATA_OPS =
 sig
   type 'a A
   type 'a T
   type 'a V
   type 'a P
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
   val properties: Properties.T T
   val string: string T
   val int: int T
   val bool: bool T
   val unit: unit T
   val pair: 'a T -> 'b T -> ('a * 'b) T
   val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   val list: 'a T -> 'a list T
   val option: 'a T -> 'a option T
   val variant: 'a V list -> 'a T
 end;
 
 signature XML =
 sig
   type attributes = (string * string) list
   datatype tree =
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
+  val string: string -> body
   val blob: string list -> body
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
   val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
   val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
   val add_content: tree -> Buffer.T -> Buffer.T
   val content_of: body -> string
   val trim_blanks: body -> body
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
   val output_markup: Markup.T -> Markup.output
   val string_of: tree -> string
   val pretty: int -> tree -> Pretty.T
   val parse_comments: string list -> unit * string list
   val parse_string : string -> string option
   val parse_element: string list -> tree * string list
   val parse_document: string list -> tree * string list
   val parse: string -> tree
   exception XML_ATOM of string
   exception XML_BODY of body
   structure Encode:
   sig
     include XML_DATA_OPS
     val tree: tree T
   end
   structure Decode:
   sig
     include XML_DATA_OPS
     val tree: tree T
   end
 end;
 
 structure XML: XML =
 struct
 
 (** XML trees **)
 
 open Output_Primitives.XML;
 
+fun string "" = []
+  | string s = [Text s];
+
 val blob = map Text;
 
 fun is_empty (Text "") = true
   | is_empty _ = false;
 
 val is_empty_body = forall is_empty;
 
 
 (* wrapped elements *)
 
 val xml_elemN = "xml_elem";
 val xml_nameN = "xml_name";
 val xml_bodyN = "xml_body";
 
 fun wrap_elem (((a, atts), body1), body2) =
   Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
 
 fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
       if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
       then SOME (((a, atts), body1), body2) else NONE
   | unwrap_elem _ = NONE;
 
 
 (* text content *)
 
 fun add_content tree =
   (case unwrap_elem tree of
     SOME (_, ts) => fold add_content ts
   | NONE =>
       (case tree of
         Elem (_, ts) => fold add_content ts
       | Text s => Buffer.add s));
 
 val content_of = Buffer.build_content o fold add_content;
 
 
 (* trim blanks *)
 
 fun trim_blanks trees =
   trees |> maps
     (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
-      | Text s =>
-          let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
-          in if s' = "" then [] else [Text s'] end);
+      | Text s => s |> raw_explode |> trim Symbol.is_blank |> implode |> string);
 
 
 
 (** string representation **)
 
 val header = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n";
 
 
 (* escaped text *)
 
 fun decode "&lt;" = "<"
   | decode "&gt;" = ">"
   | decode "&amp;" = "&"
   | decode "&apos;" = "'"
   | decode "&quot;" = "\""
   | decode c = c;
 
 fun encode "<" = "&lt;"
   | encode ">" = "&gt;"
   | encode "&" = "&amp;"
   | encode "'" = "&apos;"
   | encode "\"" = "&quot;"
   | encode c = c;
 
 val text = translate_string encode;
 
 
 (* elements *)
 
 fun elem name atts =
   space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
 
 fun element name atts body =
   let val b = implode body in
     if b = "" then enclose "<" "/>" (elem name atts)
     else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
   end;
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
 (* output content *)
 
 fun content_depth depth =
   let
     fun traverse _ (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
       | traverse d (Elem ((name, atts), ts)) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           traverse_body d ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
       | traverse _ (Text s) = Buffer.add (text s)
     and traverse_body 0 _ = Buffer.add "..."
       | traverse_body d ts = fold (traverse (d - 1)) ts;
   in Buffer.build_content o traverse depth end;
 
 val string_of = content_depth ~1;
 
 fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
 
 val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
 
 
 
 (** XML parsing **)
 
 local
 
 fun err msg (xs, _) =
   fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
 
 fun ignored _ = [];
 
 fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
 fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
 val parse_name = Scan.one name_start_char ::: Scan.many name_char;
 
 val blanks = Scan.many Symbol.is_blank;
 val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
 val regular = Scan.one Symbol.not_eof;
 fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
 
 val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
 
 val parse_cdata =
   Scan.this_string "<![CDATA[" |--
   (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
   Scan.this_string "]]>";
 
 val parse_att =
   ((parse_name >> implode) --| (blanks -- $$ "=" -- blanks)) --
   (($$ "\"" || $$ "'") :|-- (fn s =>
     (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
 
 val parse_comment =
   Scan.this_string "<!--" --
   Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
   Scan.this_string "-->" >> ignored;
 
 val parse_processing_instruction =
   Scan.this_string "<?" --
   Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
   Scan.this_string "?>" >> ignored;
 
 val parse_doctype =
   Scan.this_string "<!DOCTYPE" --
   Scan.repeat (Scan.unless ($$ ">") regular) --
   $$ ">" >> ignored;
 
 val parse_misc =
   Scan.one Symbol.is_blank >> ignored ||
   parse_processing_instruction ||
   parse_comment;
 
 val parse_optional_text =
   Scan.optional (parse_chars >> (single o Text)) [];
 
 in
 
 val parse_comments =
   blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
 
 val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
 
 fun parse_content xs =
   (parse_optional_text @@@
     Scan.repeats
       ((parse_element >> single ||
         parse_cdata >> (single o Text) ||
         parse_processing_instruction ||
         parse_comment)
       @@@ parse_optional_text)) xs
 
 and parse_element xs =
   ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
     (fn (name, _) =>
       !! (err (fn () => "Expected > or />"))
        ($$ "/" -- $$ ">" >> ignored ||
         $$ ">" |-- parse_content --|
           !! (err (fn () => "Expected </" ^ implode name ^ ">"))
               ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
     >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
 
 val parse_document =
   (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
   |-- parse_element;
 
 fun parse s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
       (blanks |-- parse_document --| blanks))) (raw_explode s) of
     (x, []) => x
   | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys));
 
 end;
 
 
 
 (** XML as data representation language **)
 
 exception XML_ATOM of string;
 exception XML_BODY of tree list;
 
 
 structure Encode =
 struct
 
 type 'a A = 'a -> string;
 type 'a T = 'a -> body;
 type 'a V = 'a -> string list * body;
 type 'a P = 'a -> string list;
 
 
 (* atomic values *)
 
 fun int_atom i = Value.print_int i;
 
 fun bool_atom false = "0"
   | bool_atom true = "1";
 
 fun unit_atom () = "";
 
 
 (* structural nodes *)
 
 fun node ts = Elem ((":", []), ts);
 
 fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
 
 fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
 
 
 (* representation of standard types *)
 
 fun tree (t: tree) = [t];
 
 fun properties props = [Elem ((":", props), [])];
 
 fun string "" = []
   | string s = [Text s];
 
 val int = string o int_atom;
 
 val bool = string o bool_atom;
 
 val unit = string o unit_atom;
 
 fun pair f g (x, y) = [node (f x), node (g y)];
 
 fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
 
 fun list f xs = map (node o f) xs;
 
 fun option _ NONE = []
   | option f (SOME x) = [node (f x)];
 
 fun variant fs x =
   [tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))];
 
 end;
 
 
 structure Decode =
 struct
 
 type 'a A = string -> 'a;
 type 'a T = body -> 'a;
 type 'a V = string list * body -> 'a;
 type 'a P = string list -> 'a;
 
 
 (* atomic values *)
 
 fun int_atom s =
   Value.parse_int s
     handle Fail _ => raise XML_ATOM s;
 
 fun bool_atom "0" = false
   | bool_atom "1" = true
   | bool_atom s = raise XML_ATOM s;
 
 fun unit_atom "" = ()
   | unit_atom s = raise XML_ATOM s;
 
 
 (* structural nodes *)
 
 fun node (Elem ((":", []), ts)) = ts
   | node t = raise XML_BODY [t];
 
 fun vector atts =
   map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
 
 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];
 
 
 (* representation of standard types *)
 
 fun tree [t] = t
   | tree ts = raise XML_BODY ts;
 
 fun properties [Elem ((":", props), [])] = props
   | properties ts = raise XML_BODY ts;
 
 fun string [] = ""
   | string [Text s] = s
   | string ts = raise XML_BODY ts;
 
 val int = int_atom o string;
 
 val bool = bool_atom o string;
 
 val unit = unit_atom o string;
 
 fun pair f g [t1, t2] = (f (node t1), g (node t2))
   | pair _ _ ts = raise XML_BODY ts;
 
 fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   | triple _ _ _ ts = raise XML_BODY ts;
 
 fun list f ts = map (f o node) ts;
 
 fun option _ [] = NONE
   | option f [t] = SOME (f (node t))
   | option _ ts = raise XML_BODY ts;
 
 fun variant fs [t] =
       let
         val (tag, (xs, ts)) = tagged t;
         val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
       in f (xs, ts) end
   | variant _ ts = raise XML_BODY ts;
 
 end;
 
 end;
diff --git a/src/Pure/PIDE/xml.scala b/src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala
+++ b/src/Pure/PIDE/xml.scala
@@ -1,459 +1,461 @@
 /*  Title:      Pure/PIDE/xml.scala
     Author:     Makarius
 
 Untyped XML trees and basic data representation.
 */
 
 package isabelle
 
 
 object XML
 {
   /** XML trees **/
 
   /* datatype representation */
 
   type Attribute = Properties.Entry
   type Attributes = Properties.T
 
   sealed abstract class Tree { override def toString: String = string_of_tree(this) }
   type Body = List[Tree]
   case class Elem(markup: Markup, body: Body) extends Tree
   {
     private lazy val hash: Int = (markup, body).hashCode()
     override def hashCode(): Int = hash
 
     def name: String = markup.name
 
     def update_attributes(more_attributes: Attributes): Elem =
       if (more_attributes.isEmpty) this
       else Elem(markup.update_properties(more_attributes), body)
 
     def + (att: Attribute): Elem = Elem(markup + att, body)
   }
   case class Text(content: String) extends Tree
   {
     private lazy val hash: Int = content.hashCode()
     override def hashCode(): Int = hash
   }
 
   def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
   def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
   def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
 
   val no_text: Text = Text("")
   val newline: Text = Text("\n")
 
+  def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
+
 
   /* name space */
 
   object Namespace
   {
     def apply(prefix: String, target: String): Namespace =
       new Namespace(prefix, target)
   }
 
   final class Namespace private(prefix: String, target: String)
   {
     def apply(name: String): String = prefix + ":" + name
     val attribute: XML.Attribute = ("xmlns:" + prefix, target)
 
     override def toString: String = attribute.toString
   }
 
 
   /* wrapped elements */
 
   val XML_ELEM = "xml_elem"
   val XML_NAME = "xml_name"
   val XML_BODY = "xml_body"
 
   object Wrapped_Elem
   {
     def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
       XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
         XML.Elem(Markup(XML_BODY, Nil), body1) :: body2)
 
     def unapply(tree: Tree): Option[(Markup, Body, Body)] =
       tree match {
         case
           XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
             XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
           Some(Markup(name, props), body1, body2)
         case _ => None
       }
   }
 
   object Root_Elem
   {
     def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body)
     def unapply(tree: Tree): Option[Body] =
       tree match {
         case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body)
         case _ => None
       }
   }
 
 
   /* traverse text */
 
   def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
   {
     def traverse(x: A, t: Tree): A =
       t match {
         case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
         case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
         case XML.Text(s) => op(x, s)
       }
     body.foldLeft(a)(traverse)
   }
 
   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
   def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
 
 
   /* text content */
 
   def content(body: Body): String =
   {
     val text = new StringBuilder(text_length(body))
     traverse_text(body)(()) { case (_, s) => text.append(s) }
     text.toString
   }
 
   def content(tree: Tree): String = content(List(tree))
 
 
 
   /** string representation **/
 
   val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
 
   def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit =
   {
     c match {
       case '<' => s ++= "&lt;"
       case '>' => s ++= "&gt;"
       case '&' => s ++= "&amp;"
       case '"' if !permissive => s ++= "&quot;"
       case '\'' if !permissive => s ++= "&apos;"
       case _ => s += c
     }
   }
 
   def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit =
   {
     if (str == null) s ++= str
     else str.iterator.foreach(output_char(s, _, permissive = permissive))
   }
 
   def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit =
   {
     s += '<'
     s ++= markup.name
     for ((a, b) <- markup.properties) {
       s += ' '
       s ++= a
       s += '='
       s += '"'
       output_string(s, b)
       s += '"'
     }
     if (end) s += '/'
     s += '>'
   }
 
   def output_elem_end(s: StringBuilder, name: String): Unit =
   {
     s += '<'
     s += '/'
     s ++= name
     s += '>'
   }
 
   def string_of_body(body: Body): String =
   {
     val s = new StringBuilder
 
     def tree(t: Tree): Unit =
       t match {
         case XML.Elem(markup, Nil) =>
           output_elem(s, markup, end = true)
         case XML.Elem(markup, ts) =>
           output_elem(s, markup)
           ts.foreach(tree)
           output_elem_end(s, markup.name)
         case XML.Text(txt) => output_string(s, txt)
       }
     body.foreach(tree)
     s.toString
   }
 
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
   def text(s: String): String = string_of_tree(XML.Text(s))
 
 
   /** cache **/
 
   object Cache
   {
     def make(
         xz: XZ.Cache = XZ.Cache.make(),
         max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
       new Cache(xz, max_string, initial_size)
 
     val none: Cache = make(XZ.Cache.none, max_string = 0)
   }
 
   class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int)
     extends isabelle.Cache(max_string, initial_size)
   {
     protected def cache_props(x: Properties.T): Properties.T =
     {
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
           case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
         }
     }
 
     protected def cache_markup(x: Markup): Markup =
     {
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case Markup(name, props) =>
               store(Markup(cache_string(name), cache_props(props)))
           }
       }
     }
 
     protected def cache_tree(x: XML.Tree): XML.Tree =
     {
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case XML.Elem(markup, body) =>
               store(XML.Elem(cache_markup(markup), cache_body(body)))
             case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
     }
 
     protected def cache_body(x: XML.Body): XML.Body =
     {
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
           case None => x.map(cache_tree)
         }
     }
 
     // support hash-consing
     def tree0(x: XML.Tree): XML.Tree =
       if (no_cache) x else synchronized { lookup(x) getOrElse store(x) }
 
     // main methods
     def props(x: Properties.T): Properties.T =
       if (no_cache) x else synchronized { cache_props(x) }
     def markup(x: Markup): Markup =
       if (no_cache) x else synchronized { cache_markup(x) }
     def tree(x: XML.Tree): XML.Tree =
       if (no_cache) x else synchronized { cache_tree(x) }
     def body(x: XML.Body): XML.Body =
       if (no_cache) x else synchronized { cache_body(x) }
     def elem(x: XML.Elem): XML.Elem =
       if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
   }
 
 
 
   /** XML as data representation language **/
 
   abstract class Error(s: String) extends Exception(s)
   class XML_Atom(s: String) extends Error(s)
   class XML_Body(body: XML.Body) extends Error("")
 
   object Encode
   {
     type T[A] = A => XML.Body
     type V[A] = PartialFunction[A, (List[String], XML.Body)]
     type P[A] = PartialFunction[A, List[String]]
 
 
     /* atomic values */
 
     def long_atom(i: Long): String = Library.signed_string_of_long(i)
 
     def int_atom(i: Int): String = Library.signed_string_of_int(i)
 
     def bool_atom(b: Boolean): String = if (b) "1" else "0"
 
     def unit_atom(u: Unit) = ""
 
 
     /* structural nodes */
 
     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
     private def vector(xs: List[String]): XML.Attributes =
       xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
 
     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
 
 
     /* representation of standard types */
 
     val tree: T[XML.Tree] = (t => List(t))
 
     val properties: T[Properties.T] =
       (props => List(XML.Elem(Markup(":", props), Nil)))
 
     val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
 
     val long: T[Long] = (x => string(long_atom(x)))
 
     val int: T[Int] = (x => string(int_atom(x)))
 
     val bool: T[Boolean] = (x => string(bool_atom(x)))
 
     val unit: T[Unit] = (x => string(unit_atom(x)))
 
     def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
       (x => List(node(f(x._1)), node(g(x._2))))
 
     def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
       (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
 
     def list[A](f: T[A]): T[List[A]] =
       (xs => xs.map((x: A) => node(f(x))))
 
     def option[A](f: T[A]): T[Option[A]] =
     {
       case None => Nil
       case Some(x) => List(node(f(x)))
     }
 
     def variant[A](fs: List[V[A]]): T[A] =
     {
       case x =>
         val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
         List(tagged(tag, f(x)))
     }
   }
 
   object Decode
   {
     type T[A] = XML.Body => A
     type V[A] = (List[String], XML.Body) => A
     type P[A] = PartialFunction[List[String], A]
 
 
     /* atomic values */
 
     def long_atom(s: String): Long =
       try { java.lang.Long.parseLong(s) }
       catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
     def int_atom(s: String): Int =
       try { Integer.parseInt(s) }
       catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
     def bool_atom(s: String): Boolean =
       if (s == "1") true
       else if (s == "0") false
       else throw new XML_Atom(s)
 
     def unit_atom(s: String): Unit =
       if (s == "") () else throw new XML_Atom(s)
 
 
     /* structural nodes */
 
     private def node(t: XML.Tree): XML.Body =
       t match {
         case XML.Elem(Markup(":", Nil), ts) => ts
         case _ => throw new XML_Body(List(t))
       }
 
     private def vector(atts: XML.Attributes): List[String] =
       atts.iterator.zipWithIndex.map(
         { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
 
     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
       t match {
         case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
         case _ => throw new XML_Body(List(t))
       }
 
 
     /* representation of standard types */
 
     val tree: T[XML.Tree] =
     {
       case List(t) => t
       case ts => throw new XML_Body(ts)
     }
 
     val properties: T[Properties.T] =
     {
       case List(XML.Elem(Markup(":", props), Nil)) => props
       case ts => throw new XML_Body(ts)
     }
 
     val string: T[String] =
     {
       case Nil => ""
       case List(XML.Text(s)) => s
       case ts => throw new XML_Body(ts)
     }
 
     val long: T[Long] = (x => long_atom(string(x)))
 
     val int: T[Int] = (x => int_atom(string(x)))
 
     val bool: T[Boolean] = (x => bool_atom(string(x)))
 
     val unit: T[Unit] = (x => unit_atom(string(x)))
 
     def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
     {
       case List(t1, t2) => (f(node(t1)), g(node(t2)))
       case ts => throw new XML_Body(ts)
     }
 
     def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
     {
       case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
       case ts => throw new XML_Body(ts)
     }
 
     def list[A](f: T[A]): T[List[A]] =
       (ts => ts.map(t => f(node(t))))
 
     def option[A](f: T[A]): T[Option[A]] =
     {
       case Nil => None
       case List(t) => Some(f(node(t)))
       case ts => throw new XML_Body(ts)
     }
 
     def variant[A](fs: List[V[A]]): T[A] =
     {
       case List(t) =>
         val (tag, (xs, ts)) = tagged(t)
         val f =
           try { fs(tag) }
           catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
         f(xs, ts)
       case ts => throw new XML_Body(ts)
     }
   }
 }