tuned XML modules;
authorwenzelm
Tue Jul 12 10:44:30 2011 +0200 (2011-07-12)
changeset 43767e0219ef7f84c
parent 43766 9545bb3cefac
child 43768 d52ab827d62b
tuned XML modules;
src/Pure/General/xml.ML
src/Pure/General/xml.scala
src/Pure/General/xml_data.ML
src/Pure/General/xml_data.scala
src/Pure/IsaMakefile
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/ROOT.ML
src/Pure/Thy/thy_header.scala
src/Pure/Tools/find_theorems.ML
src/Pure/build-jars
src/Pure/term.scala
src/Pure/term_xml.ML
     1.1 --- a/src/Pure/General/xml.ML	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ b/src/Pure/General/xml.ML	Tue Jul 12 10:44:30 2011 +0200
     1.3 @@ -4,6 +4,21 @@
     1.4  Simple XML tree values.
     1.5  *)
     1.6  
     1.7 +signature XML_DATA_OPS =
     1.8 +sig
     1.9 +  type 'a T
    1.10 +  val properties: Properties.T T
    1.11 +  val string: string T
    1.12 +  val int: int T
    1.13 +  val bool: bool T
    1.14 +  val unit: unit T
    1.15 +  val pair: 'a T -> 'b T -> ('a * 'b) T
    1.16 +  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    1.17 +  val list: 'a T -> 'a list T
    1.18 +  val option: 'a T -> 'a option T
    1.19 +  val variant: 'a T list -> 'a T
    1.20 +end;
    1.21 +
    1.22  signature XML =
    1.23  sig
    1.24    type attributes = Properties.T
    1.25 @@ -24,6 +39,10 @@
    1.26    val parse_element: string list -> tree * string list
    1.27    val parse_document: string list -> tree * string list
    1.28    val parse: string -> tree
    1.29 +  exception XML_ATOM of string
    1.30 +  exception XML_BODY of body
    1.31 +  structure Encode: XML_DATA_OPS where type 'a T = 'a -> body
    1.32 +  structure Decode: XML_DATA_OPS where type 'a T = body -> 'a
    1.33  end;
    1.34  
    1.35  structure XML: XML =
    1.36 @@ -190,4 +209,124 @@
    1.37  
    1.38  end;
    1.39  
    1.40 +
    1.41 +
    1.42 +(** XML as data representation language **)
    1.43 +
    1.44 +exception XML_ATOM of string;
    1.45 +exception XML_BODY of tree list;
    1.46 +
    1.47 +
    1.48 +structure Encode =
    1.49 +struct
    1.50 +
    1.51 +type 'a T = 'a -> body;
    1.52 +
    1.53 +
    1.54 +(* basic values *)
    1.55 +
    1.56 +fun int_atom i = signed_string_of_int i;
    1.57 +
    1.58 +fun bool_atom false = "0"
    1.59 +  | bool_atom true = "1";
    1.60 +
    1.61 +fun unit_atom () = "";
    1.62 +
    1.63 +
    1.64 +(* structural nodes *)
    1.65 +
    1.66 +fun node ts = Elem ((":", []), ts);
    1.67 +
    1.68 +fun tagged (tag, ts) = Elem ((int_atom tag, []), ts);
    1.69 +
    1.70 +
    1.71 +(* representation of standard types *)
    1.72 +
    1.73 +fun properties props = [Elem ((":", props), [])];
    1.74 +
    1.75 +fun string "" = []
    1.76 +  | string s = [Text s];
    1.77 +
    1.78 +val int = string o int_atom;
    1.79 +
    1.80 +val bool = string o bool_atom;
    1.81 +
    1.82 +val unit = string o unit_atom;
    1.83 +
    1.84 +fun pair f g (x, y) = [node (f x), node (g y)];
    1.85 +
    1.86 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
    1.87 +
    1.88 +fun list f xs = map (node o f) xs;
    1.89 +
    1.90 +fun option _ NONE = []
    1.91 +  | option f (SOME x) = [node (f x)];
    1.92 +
    1.93 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
    1.94 +
    1.95  end;
    1.96 +
    1.97 +
    1.98 +structure Decode =
    1.99 +struct
   1.100 +
   1.101 +type 'a T = body -> 'a;
   1.102 +
   1.103 +
   1.104 +(* basic values *)
   1.105 +
   1.106 +fun int_atom s =
   1.107 +  (case Int.fromString s of
   1.108 +    SOME i => i
   1.109 +  | NONE => raise XML_ATOM s);
   1.110 +
   1.111 +fun bool_atom "0" = false
   1.112 +  | bool_atom "1" = true
   1.113 +  | bool_atom s = raise XML_ATOM s;
   1.114 +
   1.115 +fun unit_atom "" = ()
   1.116 +  | unit_atom s = raise XML_ATOM s;
   1.117 +
   1.118 +
   1.119 +(* structural nodes *)
   1.120 +
   1.121 +fun node (Elem ((":", []), ts)) = ts
   1.122 +  | node t = raise XML_BODY [t];
   1.123 +
   1.124 +fun tagged (Elem ((s, []), ts)) = (int_atom s, ts)
   1.125 +  | tagged t = raise XML_BODY [t];
   1.126 +
   1.127 +
   1.128 +(* representation of standard types *)
   1.129 +
   1.130 +fun properties [Elem ((":", props), [])] = props
   1.131 +  | properties ts = raise XML_BODY ts;
   1.132 +
   1.133 +fun string [] = ""
   1.134 +  | string [Text s] = s
   1.135 +  | string ts = raise XML_BODY ts;
   1.136 +
   1.137 +val int = int_atom o string;
   1.138 +
   1.139 +val bool = bool_atom o string;
   1.140 +
   1.141 +val unit = unit_atom o string;
   1.142 +
   1.143 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
   1.144 +  | pair _ _ ts = raise XML_BODY ts;
   1.145 +
   1.146 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   1.147 +  | triple _ _ _ ts = raise XML_BODY ts;
   1.148 +
   1.149 +fun list f ts = map (f o node) ts;
   1.150 +
   1.151 +fun option _ [] = NONE
   1.152 +  | option f [t] = SOME (f (node t))
   1.153 +  | option _ ts = raise XML_BODY ts;
   1.154 +
   1.155 +fun variant fs [t] = uncurry (nth fs) (tagged t)
   1.156 +  | variant _ ts = raise XML_BODY ts;
   1.157 +
   1.158 +end;
   1.159 +
   1.160 +end;
     2.1 --- a/src/Pure/General/xml.scala	Tue Jul 12 16:00:05 2011 +0900
     2.2 +++ b/src/Pure/General/xml.scala	Tue Jul 12 10:44:30 2011 +0200
     2.3 @@ -16,6 +16,8 @@
     2.4  
     2.5  object XML
     2.6  {
     2.7 +  /** XML trees **/
     2.8 +
     2.9    /* datatype representation */
    2.10  
    2.11    type Attributes = List[(String, String)]
    2.12 @@ -174,7 +176,8 @@
    2.13    }
    2.14  
    2.15  
    2.16 -  /* document object model (W3C DOM) */
    2.17 +
    2.18 +  /** document object model (W3C DOM) **/
    2.19  
    2.20    def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
    2.21      node.getUserData(Markup.Data.name) match {
    2.22 @@ -200,4 +203,166 @@
    2.23      }
    2.24      DOM(tree)
    2.25    }
    2.26 +
    2.27 +
    2.28 +
    2.29 +  /** XML as data representation language **/
    2.30 +
    2.31 +  class XML_Atom(s: String) extends Exception(s)
    2.32 +  class XML_Body(body: XML.Body) extends Exception
    2.33 +
    2.34 +  object Encode
    2.35 +  {
    2.36 +    type T[A] = A => XML.Body
    2.37 +
    2.38 +
    2.39 +    /* basic values */
    2.40 +
    2.41 +    private def long_atom(i: Long): String = i.toString
    2.42 +
    2.43 +    private def int_atom(i: Int): String = i.toString
    2.44 +
    2.45 +    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
    2.46 +
    2.47 +    private def unit_atom(u: Unit) = ""
    2.48 +
    2.49 +
    2.50 +    /* structural nodes */
    2.51 +
    2.52 +    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    2.53 +
    2.54 +    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
    2.55 +      XML.Elem(Markup(int_atom(tag), Nil), ts)
    2.56 +
    2.57 +
    2.58 +    /* representation of standard types */
    2.59 +
    2.60 +    val properties: T[List[(String, String)]] =
    2.61 +      (props => List(XML.Elem(Markup(":", props), Nil)))
    2.62 +
    2.63 +    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
    2.64 +
    2.65 +    val long: T[Long] = (x => string(long_atom(x)))
    2.66 +
    2.67 +    val int: T[Int] = (x => string(int_atom(x)))
    2.68 +
    2.69 +    val bool: T[Boolean] = (x => string(bool_atom(x)))
    2.70 +
    2.71 +    val unit: T[Unit] = (x => string(unit_atom(x)))
    2.72 +
    2.73 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
    2.74 +      (x => List(node(f(x._1)), node(g(x._2))))
    2.75 +
    2.76 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
    2.77 +      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
    2.78 +
    2.79 +    def list[A](f: T[A]): T[List[A]] =
    2.80 +      (xs => xs.map((x: A) => node(f(x))))
    2.81 +
    2.82 +    def option[A](f: T[A]): T[Option[A]] =
    2.83 +    {
    2.84 +      case None => Nil
    2.85 +      case Some(x) => List(node(f(x)))
    2.86 +    }
    2.87 +
    2.88 +    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
    2.89 +    {
    2.90 +      case x =>
    2.91 +        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
    2.92 +        List(tagged(tag, f(x)))
    2.93 +    }
    2.94 +  }
    2.95 +
    2.96 +  object Decode
    2.97 +  {
    2.98 +    type T[A] = XML.Body => A
    2.99 +
   2.100 +
   2.101 +     /* basic values */
   2.102 +
   2.103 +    private def long_atom(s: String): Long =
   2.104 +      try { java.lang.Long.parseLong(s) }
   2.105 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   2.106 +
   2.107 +    private def int_atom(s: String): Int =
   2.108 +      try { Integer.parseInt(s) }
   2.109 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   2.110 +
   2.111 +    private def bool_atom(s: String): Boolean =
   2.112 +      if (s == "1") true
   2.113 +      else if (s == "0") false
   2.114 +      else throw new XML_Atom(s)
   2.115 +
   2.116 +    private def unit_atom(s: String): Unit =
   2.117 +      if (s == "") () else throw new XML_Atom(s)
   2.118 +
   2.119 +
   2.120 +    /* structural nodes */
   2.121 +
   2.122 +    private def node(t: XML.Tree): XML.Body =
   2.123 +      t match {
   2.124 +        case XML.Elem(Markup(":", Nil), ts) => ts
   2.125 +        case _ => throw new XML_Body(List(t))
   2.126 +      }
   2.127 +
   2.128 +    private def tagged(t: XML.Tree): (Int, XML.Body) =
   2.129 +      t match {
   2.130 +        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
   2.131 +        case _ => throw new XML_Body(List(t))
   2.132 +      }
   2.133 +
   2.134 +
   2.135 +    /* representation of standard types */
   2.136 +
   2.137 +    val properties: T[List[(String, String)]] =
   2.138 +    {
   2.139 +      case List(XML.Elem(Markup(":", props), Nil)) => props
   2.140 +      case ts => throw new XML_Body(ts)
   2.141 +    }
   2.142 +
   2.143 +    val string: T[String] =
   2.144 +    {
   2.145 +      case Nil => ""
   2.146 +      case List(XML.Text(s)) => s
   2.147 +      case ts => throw new XML_Body(ts)
   2.148 +    }
   2.149 +
   2.150 +    val long: T[Long] = (x => long_atom(string(x)))
   2.151 +
   2.152 +    val int: T[Int] = (x => int_atom(string(x)))
   2.153 +
   2.154 +    val bool: T[Boolean] = (x => bool_atom(string(x)))
   2.155 +
   2.156 +    val unit: T[Unit] = (x => unit_atom(string(x)))
   2.157 +
   2.158 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   2.159 +    {
   2.160 +      case List(t1, t2) => (f(node(t1)), g(node(t2)))
   2.161 +      case ts => throw new XML_Body(ts)
   2.162 +    }
   2.163 +
   2.164 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   2.165 +    {
   2.166 +      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   2.167 +      case ts => throw new XML_Body(ts)
   2.168 +    }
   2.169 +
   2.170 +    def list[A](f: T[A]): T[List[A]] =
   2.171 +      (ts => ts.map(t => f(node(t))))
   2.172 +
   2.173 +    def option[A](f: T[A]): T[Option[A]] =
   2.174 +    {
   2.175 +      case Nil => None
   2.176 +      case List(t) => Some(f(node(t)))
   2.177 +      case ts => throw new XML_Body(ts)
   2.178 +    }
   2.179 +
   2.180 +    def variant[A](fs: List[T[A]]): T[A] =
   2.181 +    {
   2.182 +      case List(t) =>
   2.183 +        val (tag, ts) = tagged(t)
   2.184 +        fs(tag)(ts)
   2.185 +      case ts => throw new XML_Body(ts)
   2.186 +    }
   2.187 +  }
   2.188  }
     3.1 --- a/src/Pure/General/xml_data.ML	Tue Jul 12 16:00:05 2011 +0900
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,154 +0,0 @@
     3.4 -(*  Title:      Pure/General/xml_data.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -XML as basic data representation language.
     3.8 -*)
     3.9 -
    3.10 -signature XML_DATA_OPS =
    3.11 -sig
    3.12 -  type 'a T
    3.13 -  val properties: Properties.T T
    3.14 -  val string: string T
    3.15 -  val int: int T
    3.16 -  val bool: bool T
    3.17 -  val unit: unit T
    3.18 -  val pair: 'a T -> 'b T -> ('a * 'b) T
    3.19 -  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    3.20 -  val list: 'a T -> 'a list T
    3.21 -  val option: 'a T -> 'a option T
    3.22 -  val variant: 'a T list -> 'a T
    3.23 -end;
    3.24 -
    3.25 -signature XML_DATA =
    3.26 -sig
    3.27 -  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
    3.28 -  exception XML_ATOM of string
    3.29 -  exception XML_BODY of XML.body
    3.30 -  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
    3.31 -end;
    3.32 -
    3.33 -structure XML_Data: XML_DATA =
    3.34 -struct
    3.35 -
    3.36 -(** encode **)
    3.37 -
    3.38 -structure Encode =
    3.39 -struct
    3.40 -
    3.41 -type 'a T = 'a -> XML.body;
    3.42 -
    3.43 -
    3.44 -(* basic values *)
    3.45 -
    3.46 -fun int_atom i = signed_string_of_int i;
    3.47 -
    3.48 -fun bool_atom false = "0"
    3.49 -  | bool_atom true = "1";
    3.50 -
    3.51 -fun unit_atom () = "";
    3.52 -
    3.53 -
    3.54 -(* structural nodes *)
    3.55 -
    3.56 -fun node ts = XML.Elem ((":", []), ts);
    3.57 -
    3.58 -fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
    3.59 -
    3.60 -
    3.61 -(* representation of standard types *)
    3.62 -
    3.63 -fun properties props = [XML.Elem ((":", props), [])];
    3.64 -
    3.65 -fun string "" = []
    3.66 -  | string s = [XML.Text s];
    3.67 -
    3.68 -val int = string o int_atom;
    3.69 -
    3.70 -val bool = string o bool_atom;
    3.71 -
    3.72 -val unit = string o unit_atom;
    3.73 -
    3.74 -fun pair f g (x, y) = [node (f x), node (g y)];
    3.75 -
    3.76 -fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
    3.77 -
    3.78 -fun list f xs = map (node o f) xs;
    3.79 -
    3.80 -fun option _ NONE = []
    3.81 -  | option f (SOME x) = [node (f x)];
    3.82 -
    3.83 -fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
    3.84 -
    3.85 -end;
    3.86 -
    3.87 -
    3.88 -
    3.89 -(** decode **)
    3.90 -
    3.91 -exception XML_ATOM of string;
    3.92 -exception XML_BODY of XML.tree list;
    3.93 -
    3.94 -structure Decode =
    3.95 -struct
    3.96 -
    3.97 -type 'a T = XML.body -> 'a;
    3.98 -
    3.99 -
   3.100 -(* basic values *)
   3.101 -
   3.102 -fun int_atom s =
   3.103 -  (case Int.fromString s of
   3.104 -    SOME i => i
   3.105 -  | NONE => raise XML_ATOM s);
   3.106 -
   3.107 -fun bool_atom "0" = false
   3.108 -  | bool_atom "1" = true
   3.109 -  | bool_atom s = raise XML_ATOM s;
   3.110 -
   3.111 -fun unit_atom "" = ()
   3.112 -  | unit_atom s = raise XML_ATOM s;
   3.113 -
   3.114 -
   3.115 -(* structural nodes *)
   3.116 -
   3.117 -fun node (XML.Elem ((":", []), ts)) = ts
   3.118 -  | node t = raise XML_BODY [t];
   3.119 -
   3.120 -fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
   3.121 -  | tagged t = raise XML_BODY [t];
   3.122 -
   3.123 -
   3.124 -(* representation of standard types *)
   3.125 -
   3.126 -fun properties [XML.Elem ((":", props), [])] = props
   3.127 -  | properties ts = raise XML_BODY ts;
   3.128 -
   3.129 -fun string [] = ""
   3.130 -  | string [XML.Text s] = s
   3.131 -  | string ts = raise XML_BODY ts;
   3.132 -
   3.133 -val int = int_atom o string;
   3.134 -
   3.135 -val bool = bool_atom o string;
   3.136 -
   3.137 -val unit = unit_atom o string;
   3.138 -
   3.139 -fun pair f g [t1, t2] = (f (node t1), g (node t2))
   3.140 -  | pair _ _ ts = raise XML_BODY ts;
   3.141 -
   3.142 -fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   3.143 -  | triple _ _ _ ts = raise XML_BODY ts;
   3.144 -
   3.145 -fun list f ts = map (f o node) ts;
   3.146 -
   3.147 -fun option _ [] = NONE
   3.148 -  | option f [t] = SOME (f (node t))
   3.149 -  | option _ ts = raise XML_BODY ts;
   3.150 -
   3.151 -fun variant fs [t] = uncurry (nth fs) (tagged t)
   3.152 -  | variant _ ts = raise XML_BODY ts;
   3.153 -
   3.154 -end;
   3.155 -
   3.156 -end;
   3.157 -
     4.1 --- a/src/Pure/General/xml_data.scala	Tue Jul 12 16:00:05 2011 +0900
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,176 +0,0 @@
     4.4 -/*  Title:      Pure/General/xml_data.scala
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -XML as basic data representation language.
     4.8 -*/
     4.9 -
    4.10 -package isabelle
    4.11 -
    4.12 -
    4.13 -
    4.14 -object XML_Data
    4.15 -{
    4.16 -  /** encode **/
    4.17 -
    4.18 -  object Encode
    4.19 -  {
    4.20 -    type T[A] = A => XML.Body
    4.21 -
    4.22 -
    4.23 -    /* basic values */
    4.24 -
    4.25 -    private def long_atom(i: Long): String = i.toString
    4.26 -
    4.27 -    private def int_atom(i: Int): String = i.toString
    4.28 -
    4.29 -    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
    4.30 -
    4.31 -    private def unit_atom(u: Unit) = ""
    4.32 -
    4.33 -
    4.34 -    /* structural nodes */
    4.35 -
    4.36 -    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    4.37 -
    4.38 -    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
    4.39 -      XML.Elem(Markup(int_atom(tag), Nil), ts)
    4.40 -
    4.41 -
    4.42 -    /* representation of standard types */
    4.43 -
    4.44 -    val properties: T[List[(String, String)]] =
    4.45 -      (props => List(XML.Elem(Markup(":", props), Nil)))
    4.46 -
    4.47 -    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
    4.48 -
    4.49 -    val long: T[Long] = (x => string(long_atom(x)))
    4.50 -
    4.51 -    val int: T[Int] = (x => string(int_atom(x)))
    4.52 -
    4.53 -    val bool: T[Boolean] = (x => string(bool_atom(x)))
    4.54 -
    4.55 -    val unit: T[Unit] = (x => string(unit_atom(x)))
    4.56 -
    4.57 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
    4.58 -      (x => List(node(f(x._1)), node(g(x._2))))
    4.59 -
    4.60 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
    4.61 -      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
    4.62 -
    4.63 -    def list[A](f: T[A]): T[List[A]] =
    4.64 -      (xs => xs.map((x: A) => node(f(x))))
    4.65 -
    4.66 -    def option[A](f: T[A]): T[Option[A]] =
    4.67 -    {
    4.68 -      case None => Nil
    4.69 -      case Some(x) => List(node(f(x)))
    4.70 -    }
    4.71 -
    4.72 -    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
    4.73 -    {
    4.74 -      case x =>
    4.75 -        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
    4.76 -        List(tagged(tag, f(x)))
    4.77 -    }
    4.78 -  }
    4.79 -
    4.80 -
    4.81 -
    4.82 -  /** decode **/
    4.83 -
    4.84 -  class XML_Atom(s: String) extends Exception(s)
    4.85 -  class XML_Body(body: XML.Body) extends Exception
    4.86 -
    4.87 -  object Decode
    4.88 -  {
    4.89 -    type T[A] = XML.Body => A
    4.90 -
    4.91 -
    4.92 -     /* basic values */
    4.93 -
    4.94 -    private def long_atom(s: String): Long =
    4.95 -      try { java.lang.Long.parseLong(s) }
    4.96 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
    4.97 -
    4.98 -    private def int_atom(s: String): Int =
    4.99 -      try { Integer.parseInt(s) }
   4.100 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   4.101 -
   4.102 -    private def bool_atom(s: String): Boolean =
   4.103 -      if (s == "1") true
   4.104 -      else if (s == "0") false
   4.105 -      else throw new XML_Atom(s)
   4.106 -
   4.107 -    private def unit_atom(s: String): Unit =
   4.108 -      if (s == "") () else throw new XML_Atom(s)
   4.109 -
   4.110 -
   4.111 -    /* structural nodes */
   4.112 -
   4.113 -    private def node(t: XML.Tree): XML.Body =
   4.114 -      t match {
   4.115 -        case XML.Elem(Markup(":", Nil), ts) => ts
   4.116 -        case _ => throw new XML_Body(List(t))
   4.117 -      }
   4.118 -
   4.119 -    private def tagged(t: XML.Tree): (Int, XML.Body) =
   4.120 -      t match {
   4.121 -        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
   4.122 -        case _ => throw new XML_Body(List(t))
   4.123 -      }
   4.124 -
   4.125 -
   4.126 -    /* representation of standard types */
   4.127 -
   4.128 -    val properties: T[List[(String, String)]] =
   4.129 -    {
   4.130 -      case List(XML.Elem(Markup(":", props), Nil)) => props
   4.131 -      case ts => throw new XML_Body(ts)
   4.132 -    }
   4.133 -
   4.134 -    val string: T[String] =
   4.135 -    {
   4.136 -      case Nil => ""
   4.137 -      case List(XML.Text(s)) => s
   4.138 -      case ts => throw new XML_Body(ts)
   4.139 -    }
   4.140 -
   4.141 -    val long: T[Long] = (x => long_atom(string(x)))
   4.142 -
   4.143 -    val int: T[Int] = (x => int_atom(string(x)))
   4.144 -
   4.145 -    val bool: T[Boolean] = (x => bool_atom(string(x)))
   4.146 -
   4.147 -    val unit: T[Unit] = (x => unit_atom(string(x)))
   4.148 -
   4.149 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   4.150 -    {
   4.151 -      case List(t1, t2) => (f(node(t1)), g(node(t2)))
   4.152 -      case ts => throw new XML_Body(ts)
   4.153 -    }
   4.154 -
   4.155 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   4.156 -    {
   4.157 -      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   4.158 -      case ts => throw new XML_Body(ts)
   4.159 -    }
   4.160 -
   4.161 -    def list[A](f: T[A]): T[List[A]] =
   4.162 -      (ts => ts.map(t => f(node(t))))
   4.163 -
   4.164 -    def option[A](f: T[A]): T[Option[A]] =
   4.165 -    {
   4.166 -      case Nil => None
   4.167 -      case List(t) => Some(f(node(t)))
   4.168 -      case ts => throw new XML_Body(ts)
   4.169 -    }
   4.170 -
   4.171 -    def variant[A](fs: List[T[A]]): T[A] =
   4.172 -    {
   4.173 -      case List(t) =>
   4.174 -        val (tag, ts) = tagged(t)
   4.175 -        fs(tag)(ts)
   4.176 -      case ts => throw new XML_Body(ts)
   4.177 -    }
   4.178 -  }
   4.179 -}
     5.1 --- a/src/Pure/IsaMakefile	Tue Jul 12 16:00:05 2011 +0900
     5.2 +++ b/src/Pure/IsaMakefile	Tue Jul 12 10:44:30 2011 +0200
     5.3 @@ -104,7 +104,6 @@
     5.4    General/timing.ML					\
     5.5    General/url.ML					\
     5.6    General/xml.ML					\
     5.7 -  General/xml_data.ML					\
     5.8    General/yxml.ML					\
     5.9    Isar/args.ML						\
    5.10    Isar/attrib.ML					\
     6.1 --- a/src/Pure/PIDE/isar_document.ML	Tue Jul 12 16:00:05 2011 +0900
     6.2 +++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 12 10:44:30 2011 +0200
     6.3 @@ -18,10 +18,10 @@
     6.4          val old_id = Document.parse_id old_id_string;
     6.5          val new_id = Document.parse_id new_id_string;
     6.6          val edits = YXML.parse_body edits_yxml |>
     6.7 -          let open XML_Data.Decode
     6.8 +          let open XML.Decode
     6.9            in list (pair string (option (list (pair (option int) (option int))))) end;
    6.10          val headers = YXML.parse_body headers_yxml |>
    6.11 -          let open XML_Data.Decode
    6.12 +          let open XML.Decode
    6.13            in list (pair string (triple string (list string) (list string))) end;
    6.14  
    6.15        val await_cancellation = Document.cancel_execution state;
     7.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Jul 12 16:00:05 2011 +0900
     7.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Jul 12 10:44:30 2011 +0200
     7.3 @@ -143,12 +143,12 @@
     7.4        edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
     7.5    {
     7.6      val arg1 =
     7.7 -    { import XML_Data.Encode._
     7.8 +    { import XML.Encode._
     7.9        list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
    7.10  
    7.11      val arg2 =
    7.12 -    { import XML_Data.Encode._
    7.13 -      list(pair(string, Thy_Header.encode_xml_data))(headers) }
    7.14 +    { import XML.Encode._
    7.15 +      list(pair(string, Thy_Header.xml_encode))(headers) }
    7.16  
    7.17      input("Isar_Document.edit_version",
    7.18        Document.ID(old_id), Document.ID(new_id),
     8.1 --- a/src/Pure/ROOT.ML	Tue Jul 12 16:00:05 2011 +0900
     8.2 +++ b/src/Pure/ROOT.ML	Tue Jul 12 10:44:30 2011 +0200
     8.3 @@ -53,7 +53,6 @@
     8.4  use "General/linear_set.ML";
     8.5  use "General/buffer.ML";
     8.6  use "General/xml.ML";
     8.7 -use "General/xml_data.ML";
     8.8  use "General/pretty.ML";
     8.9  use "General/path.ML";
    8.10  use "General/url.ML";
     9.1 --- a/src/Pure/Thy/thy_header.scala	Tue Jul 12 16:00:05 2011 +0900
     9.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Jul 12 10:44:30 2011 +0200
     9.3 @@ -31,10 +31,10 @@
     9.4        Header(f(name), imports.map(f), uses.map(f))
     9.5    }
     9.6  
     9.7 -  val encode_xml_data: XML_Data.Encode.T[Header] =
     9.8 +  val xml_encode: XML.Encode.T[Header] =
     9.9    {
    9.10      case Header(name, imports, uses) =>
    9.11 -      import XML_Data.Encode._
    9.12 +      import XML.Encode._
    9.13        triple(string, list(string), list(string))(name, imports, uses)
    9.14    }
    9.15  
    10.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Jul 12 16:00:05 2011 +0900
    10.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 12 10:44:30 2011 +0200
    10.3 @@ -139,8 +139,8 @@
    10.4            |> (if rem_dups then cons ("rem_dups", "") else I)
    10.5            |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    10.6        in
    10.7 -        XML.Elem (("Query", properties), XML_Data.Encode.list
    10.8 -          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
    10.9 +        XML.Elem (("Query", properties), XML.Encode.list
   10.10 +          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
   10.11        end
   10.12    | xml_of_query _ = raise Fail "cannot serialize goal";
   10.13  
   10.14 @@ -149,7 +149,7 @@
   10.15          val rem_dups = Properties.defined properties "rem_dups";
   10.16          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
   10.17          val criteria =
   10.18 -          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
   10.19 +          XML.Decode.list (XML.Decode.pair XML.Decode.bool
   10.20              (criterion_of_xml o the_single)) body;
   10.21        in
   10.22          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
   10.23 @@ -190,12 +190,12 @@
   10.24      val properties =
   10.25        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   10.26    in
   10.27 -    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
   10.28 +    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
   10.29    end;
   10.30  
   10.31  fun result_of_xml (XML.Elem (("Result", properties), body)) =
   10.32        (Properties.get properties "found" |> Option.map Markup.parse_int,
   10.33 -       XML_Data.Decode.list (theorem_of_xml o the_single) body)
   10.34 +       XML.Decode.list (theorem_of_xml o the_single) body)
   10.35    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
   10.36  
   10.37  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    11.1 --- a/src/Pure/build-jars	Tue Jul 12 16:00:05 2011 +0900
    11.2 +++ b/src/Pure/build-jars	Tue Jul 12 10:44:30 2011 +0200
    11.3 @@ -24,7 +24,6 @@
    11.4    General/sha1.scala
    11.5    General/symbol.scala
    11.6    General/xml.scala
    11.7 -  General/xml_data.scala
    11.8    General/yxml.scala
    11.9    Isar/keyword.scala
   11.10    Isar/outer_syntax.scala
    12.1 --- a/src/Pure/term.scala	Tue Jul 12 16:00:05 2011 +0900
    12.2 +++ b/src/Pure/term.scala	Tue Jul 12 10:44:30 2011 +0200
    12.3 @@ -43,7 +43,7 @@
    12.4  
    12.5    object Encode
    12.6    {
    12.7 -    import XML_Data.Encode._
    12.8 +    import XML.Encode._
    12.9  
   12.10      val indexname: T[Indexname] = pair(string, int)
   12.11  
   12.12 @@ -67,7 +67,7 @@
   12.13  
   12.14    object Decode
   12.15    {
   12.16 -    import XML_Data.Decode._
   12.17 +    import XML.Decode._
   12.18  
   12.19      val indexname: T[Indexname] = pair(string, int)
   12.20  
    13.1 --- a/src/Pure/term_xml.ML	Tue Jul 12 16:00:05 2011 +0900
    13.2 +++ b/src/Pure/term_xml.ML	Tue Jul 12 10:44:30 2011 +0200
    13.3 @@ -15,8 +15,8 @@
    13.4  
    13.5  signature TERM_XML =
    13.6  sig
    13.7 -  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
    13.8 -  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
    13.9 +  structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
   13.10 +  structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
   13.11  end;
   13.12  
   13.13  structure Term_XML: TERM_XML =
   13.14 @@ -27,7 +27,7 @@
   13.15  structure Encode =
   13.16  struct
   13.17  
   13.18 -open XML_Data.Encode;
   13.19 +open XML.Encode;
   13.20  
   13.21  val indexname = pair string int;
   13.22  
   13.23 @@ -54,7 +54,7 @@
   13.24  structure Decode =
   13.25  struct
   13.26  
   13.27 -open XML_Data.Decode;
   13.28 +open XML.Decode;
   13.29  
   13.30  val indexname = pair string int;
   13.31