# HG changeset patch
# User wenzelm
# Date 1310460270 -7200
# Node ID e0219ef7f84c7dcf171e7d77dc2a0e9ff737b397
# Parent  9545bb3cefac21c6529eec51bbe98798db306359
tuned XML modules;

diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/General/xml.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -4,6 +4,21 @@
 Simple XML tree values.
 *)
 
+signature XML_DATA_OPS =
+sig
+  type 'a T
+  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 T list -> 'a T
+end;
+
 signature XML =
 sig
   type attributes = Properties.T
@@ -24,6 +39,10 @@
   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: XML_DATA_OPS where type 'a T = 'a -> body
+  structure Decode: XML_DATA_OPS where type 'a T = body -> 'a
 end;
 
 structure XML: XML =
@@ -190,4 +209,124 @@
 
 end;
 
+
+
+(** XML as data representation language **)
+
+exception XML_ATOM of string;
+exception XML_BODY of tree list;
+
+
+structure Encode =
+struct
+
+type 'a T = 'a -> body;
+
+
+(* basic values *)
+
+fun int_atom i = signed_string_of_int i;
+
+fun bool_atom false = "0"
+  | bool_atom true = "1";
+
+fun unit_atom () = "";
+
+
+(* structural nodes *)
+
+fun node ts = Elem ((":", []), ts);
+
+fun tagged (tag, ts) = Elem ((int_atom tag, []), ts);
+
+
+(* representation of standard types *)
+
+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 => try f x) fs))];
+
 end;
+
+
+structure Decode =
+struct
+
+type 'a T = body -> 'a;
+
+
+(* basic values *)
+
+fun int_atom s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => 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 tagged (Elem ((s, []), ts)) = (int_atom s, ts)
+  | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+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] = uncurry (nth fs) (tagged t)
+  | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/General/xml.scala	Tue Jul 12 10:44:30 2011 +0200
@@ -16,6 +16,8 @@
 
 object XML
 {
+  /** XML trees **/
+
   /* datatype representation */
 
   type Attributes = List[(String, String)]
@@ -174,7 +176,8 @@
   }
 
 
-  /* document object model (W3C DOM) */
+
+  /** document object model (W3C DOM) **/
 
   def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
     node.getUserData(Markup.Data.name) match {
@@ -200,4 +203,166 @@
     }
     DOM(tree)
   }
+
+
+
+  /** XML as data representation language **/
+
+  class XML_Atom(s: String) extends Exception(s)
+  class XML_Body(body: XML.Body) extends Exception
+
+  object Encode
+  {
+    type T[A] = A => XML.Body
+
+
+    /* basic values */
+
+    private def long_atom(i: Long): String = i.toString
+
+    private def int_atom(i: Int): String = i.toString
+
+    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+    private 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)
+
+
+    /* representation of standard types */
+
+    val properties: T[List[(String, String)]] =
+      (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[PartialFunction[A, XML.Body]]): 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
+
+
+     /* basic values */
+
+    private 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 =
+      try { Integer.parseInt(s) }
+      catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+    private 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 =
+      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 tagged(t: XML.Tree): (Int, XML.Body) =
+      t match {
+        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
+        case _ => throw new XML_Body(List(t))
+      }
+
+
+    /* representation of standard types */
+
+    val properties: T[List[(String, String)]] =
+    {
+      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[T[A]]): T[A] =
+    {
+      case List(t) =>
+        val (tag, ts) = tagged(t)
+        fs(tag)(ts)
+      case ts => throw new XML_Body(ts)
+    }
+  }
 }
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/General/xml_data.ML
--- a/src/Pure/General/xml_data.ML	Tue Jul 12 16:00:05 2011 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-(*  Title:      Pure/General/xml_data.ML
-    Author:     Makarius
-
-XML as basic data representation language.
-*)
-
-signature XML_DATA_OPS =
-sig
-  type 'a T
-  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 T list -> 'a T
-end;
-
-signature XML_DATA =
-sig
-  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
-  exception XML_ATOM of string
-  exception XML_BODY of XML.body
-  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
-end;
-
-structure XML_Data: XML_DATA =
-struct
-
-(** encode **)
-
-structure Encode =
-struct
-
-type 'a T = 'a -> XML.body;
-
-
-(* basic values *)
-
-fun int_atom i = signed_string_of_int i;
-
-fun bool_atom false = "0"
-  | bool_atom true = "1";
-
-fun unit_atom () = "";
-
-
-(* structural nodes *)
-
-fun node ts = XML.Elem ((":", []), ts);
-
-fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
-
-
-(* representation of standard types *)
-
-fun properties props = [XML.Elem ((":", props), [])];
-
-fun string "" = []
-  | string s = [XML.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 => try f x) fs))];
-
-end;
-
-
-
-(** decode **)
-
-exception XML_ATOM of string;
-exception XML_BODY of XML.tree list;
-
-structure Decode =
-struct
-
-type 'a T = XML.body -> 'a;
-
-
-(* basic values *)
-
-fun int_atom s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => 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 (XML.Elem ((":", []), ts)) = ts
-  | node t = raise XML_BODY [t];
-
-fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
-  | tagged t = raise XML_BODY [t];
-
-
-(* representation of standard types *)
-
-fun properties [XML.Elem ((":", props), [])] = props
-  | properties ts = raise XML_BODY ts;
-
-fun string [] = ""
-  | string [XML.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] = uncurry (nth fs) (tagged t)
-  | variant _ ts = raise XML_BODY ts;
-
-end;
-
-end;
-
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/General/xml_data.scala
--- a/src/Pure/General/xml_data.scala	Tue Jul 12 16:00:05 2011 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-/*  Title:      Pure/General/xml_data.scala
-    Author:     Makarius
-
-XML as basic data representation language.
-*/
-
-package isabelle
-
-
-
-object XML_Data
-{
-  /** encode **/
-
-  object Encode
-  {
-    type T[A] = A => XML.Body
-
-
-    /* basic values */
-
-    private def long_atom(i: Long): String = i.toString
-
-    private def int_atom(i: Int): String = i.toString
-
-    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
-
-    private 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)
-
-
-    /* representation of standard types */
-
-    val properties: T[List[(String, String)]] =
-      (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[PartialFunction[A, XML.Body]]): T[A] =
-    {
-      case x =>
-        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
-        List(tagged(tag, f(x)))
-    }
-  }
-
-
-
-  /** decode **/
-
-  class XML_Atom(s: String) extends Exception(s)
-  class XML_Body(body: XML.Body) extends Exception
-
-  object Decode
-  {
-    type T[A] = XML.Body => A
-
-
-     /* basic values */
-
-    private 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 =
-      try { Integer.parseInt(s) }
-      catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
-    private 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 =
-      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 tagged(t: XML.Tree): (Int, XML.Body) =
-      t match {
-        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
-        case _ => throw new XML_Body(List(t))
-      }
-
-
-    /* representation of standard types */
-
-    val properties: T[List[(String, String)]] =
-    {
-      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[T[A]]): T[A] =
-    {
-      case List(t) =>
-        val (tag, ts) = tagged(t)
-        fs(tag)(ts)
-      case ts => throw new XML_Body(ts)
-    }
-  }
-}
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/IsaMakefile	Tue Jul 12 10:44:30 2011 +0200
@@ -104,7 +104,6 @@
   General/timing.ML					\
   General/url.ML					\
   General/xml.ML					\
-  General/xml_data.ML					\
   General/yxml.ML					\
   Isar/args.ML						\
   Isar/attrib.ML					\
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -18,10 +18,10 @@
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
         val edits = YXML.parse_body edits_yxml |>
-          let open XML_Data.Decode
+          let open XML.Decode
           in list (pair string (option (list (pair (option int) (option int))))) end;
         val headers = YXML.parse_body headers_yxml |>
-          let open XML_Data.Decode
+          let open XML.Decode
           in list (pair string (triple string (list string) (list string))) end;
 
       val await_cancellation = Document.cancel_execution state;
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/PIDE/isar_document.scala	Tue Jul 12 10:44:30 2011 +0200
@@ -143,12 +143,12 @@
       edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
   {
     val arg1 =
-    { import XML_Data.Encode._
+    { import XML.Encode._
       list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
 
     val arg2 =
-    { import XML_Data.Encode._
-      list(pair(string, Thy_Header.encode_xml_data))(headers) }
+    { import XML.Encode._
+      list(pair(string, Thy_Header.xml_encode))(headers) }
 
     input("Isar_Document.edit_version",
       Document.ID(old_id), Document.ID(new_id),
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/ROOT.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -53,7 +53,6 @@
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/xml.ML";
-use "General/xml_data.ML";
 use "General/pretty.ML";
 use "General/path.ML";
 use "General/url.ML";
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/Thy/thy_header.scala	Tue Jul 12 10:44:30 2011 +0200
@@ -31,10 +31,10 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
-  val encode_xml_data: XML_Data.Encode.T[Header] =
+  val xml_encode: XML.Encode.T[Header] =
   {
     case Header(name, imports, uses) =>
-      import XML_Data.Encode._
+      import XML.Encode._
       triple(string, list(string), list(string))(name, imports, uses)
   }
 
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -139,8 +139,8 @@
           |> (if rem_dups then cons ("rem_dups", "") else I)
           |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
       in
-        XML.Elem (("Query", properties), XML_Data.Encode.list
-          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
+        XML.Elem (("Query", properties), XML.Encode.list
+          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
       end
   | xml_of_query _ = raise Fail "cannot serialize goal";
 
@@ -149,7 +149,7 @@
         val rem_dups = Properties.defined properties "rem_dups";
         val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
         val criteria =
-          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
+          XML.Decode.list (XML.Decode.pair XML.Decode.bool
             (criterion_of_xml o the_single)) body;
       in
         {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
@@ -190,12 +190,12 @@
     val properties =
       if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   in
-    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
+    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
   end;
 
 fun result_of_xml (XML.Elem (("Result", properties), body)) =
       (Properties.get properties "found" |> Option.map Markup.parse_int,
-       XML_Data.Decode.list (theorem_of_xml o the_single) body)
+       XML.Decode.list (theorem_of_xml o the_single) body)
   | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
 
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/build-jars	Tue Jul 12 10:44:30 2011 +0200
@@ -24,7 +24,6 @@
   General/sha1.scala
   General/symbol.scala
   General/xml.scala
-  General/xml_data.scala
   General/yxml.scala
   Isar/keyword.scala
   Isar/outer_syntax.scala
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/term.scala
--- a/src/Pure/term.scala	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/term.scala	Tue Jul 12 10:44:30 2011 +0200
@@ -43,7 +43,7 @@
 
   object Encode
   {
-    import XML_Data.Encode._
+    import XML.Encode._
 
     val indexname: T[Indexname] = pair(string, int)
 
@@ -67,7 +67,7 @@
 
   object Decode
   {
-    import XML_Data.Decode._
+    import XML.Decode._
 
     val indexname: T[Indexname] = pair(string, int)
 
diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/term_xml.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -15,8 +15,8 @@
 
 signature TERM_XML =
 sig
-  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
-  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
+  structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
+  structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
 end;
 
 structure Term_XML: TERM_XML =
@@ -27,7 +27,7 @@
 structure Encode =
 struct
 
-open XML_Data.Encode;
+open XML.Encode;
 
 val indexname = pair string int;
 
@@ -54,7 +54,7 @@
 structure Decode =
 struct
 
-open XML_Data.Decode;
+open XML.Decode;
 
 val indexname = pair string int;