diff -r 22c87ff1b8a9 -r ce9189450447 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Jul 12 15:32:16 2011 +0200
+++ b/src/Pure/General/xml.scala	Tue Jul 12 17:53:06 2011 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/xml.scala
     Author:     Makarius
 
-Simple XML tree values.
+Untyped XML trees.
 */
 
 package isabelle
@@ -12,6 +12,7 @@
 import javax.xml.parsers.DocumentBuilderFactory
 
 import scala.actors.Actor._
+import scala.collection.mutable
 
 
 object XML
@@ -216,23 +217,26 @@
     type T[A] = A => XML.Body
 
 
-    /* basic values */
+    /* atomic values */
 
-    private def long_atom(i: Long): String = i.toString
+    def long_atom(i: Long): String = i.toString
 
-    private def int_atom(i: Int): String = i.toString
+    def int_atom(i: Int): String = i.toString
 
-    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+    def bool_atom(b: Boolean): String = if (b) "1" else "0"
 
-    private def unit_atom(u: Unit) = ""
+    def unit_atom(u: Unit) = ""
 
 
     /* structural nodes */
 
     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
-    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
-      XML.Elem(Markup(int_atom(tag), Nil), ts)
+    private def vector(xs: List[String]): List[(String, String)] =
+      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+
+    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 */
@@ -265,7 +269,7 @@
       case Some(x) => List(node(f(x)))
     }
 
-    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
+    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
     {
       case x =>
         val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
@@ -276,24 +280,25 @@
   object Decode
   {
     type T[A] = XML.Body => A
+    type V[A] = (List[String], XML.Body) => A
 
 
-     /* basic values */
+    /* atomic values */
 
-    private def long_atom(s: String): Long =
+    def long_atom(s: String): Long =
       try { java.lang.Long.parseLong(s) }
       catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
-    private def int_atom(s: String): Int =
+    def int_atom(s: String): Int =
       try { Integer.parseInt(s) }
       catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
-    private def bool_atom(s: String): Boolean =
+    def bool_atom(s: String): Boolean =
       if (s == "1") true
       else if (s == "0") false
       else throw new XML_Atom(s)
 
-    private def unit_atom(s: String): Unit =
+    def unit_atom(s: String): Unit =
       if (s == "") () else throw new XML_Atom(s)
 
 
@@ -305,9 +310,20 @@
         case _ => throw new XML_Body(List(t))
       }
 
-    private def tagged(t: XML.Tree): (Int, XML.Body) =
+    private def vector(props: List[(String, String)]): List[String] =
+    {
+      val xs = new mutable.ListBuffer[String]
+      var i = 0
+      for ((a, x) <- props) {
+        if (int_atom(a) == i) { xs += x; i = i + 1 }
+        else throw new XML_Atom(a)
+      }
+      xs.toList
+    }
+
+    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
       t match {
-        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
+        case XML.Elem(Markup(name, props), ts) => (int_atom(name), (vector(props), ts))
         case _ => throw new XML_Body(List(t))
       }
 
@@ -357,14 +373,14 @@
       case ts => throw new XML_Body(ts)
     }
 
-    def variant[A](fs: List[T[A]]): T[A] =
+    def variant[A](fs: List[V[A]]): T[A] =
     {
       case List(t) =>
-        val (tag, ts) = tagged(t)
+        val (tag, (xs, ts)) = tagged(t)
         val f =
           try { fs(tag) }
           catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
-        f(ts)
+        f(xs, ts)
       case ts => throw new XML_Body(ts)
     }
   }