simplified XML_Data;
authorwenzelm
Sun Jul 10 13:51:21 2011 +0200 (2011-07-10)
changeset 437244e58485fa320
parent 43723 8a63c95b1d5b
child 43725 bebcfcad12d4
simplified XML_Data;
src/Pure/General/xml_data.ML
src/Pure/General/xml_data.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/Thy/thy_header.scala
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/General/xml_data.ML	Sun Jul 10 13:00:22 2011 +0200
     1.2 +++ b/src/Pure/General/xml_data.ML	Sun Jul 10 13:51:21 2011 +0200
     1.3 @@ -6,137 +6,152 @@
     1.4  
     1.5  signature XML_DATA =
     1.6  sig
     1.7 +  structure Make:
     1.8 +  sig
     1.9 +    val properties: Properties.T -> XML.body
    1.10 +    val string: string -> XML.body
    1.11 +    val int: int -> XML.body
    1.12 +    val bool: bool -> XML.body
    1.13 +    val unit: unit -> XML.body
    1.14 +    val pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    1.15 +    val triple: ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    1.16 +    val list: ('a -> XML.body) -> 'a list -> XML.body
    1.17 +    val option: ('a -> XML.body) -> 'a option -> XML.body
    1.18 +    val variant: ('a -> XML.body) list -> 'a -> XML.body
    1.19 +  end
    1.20    exception XML_ATOM of string
    1.21    exception XML_BODY of XML.body
    1.22 -  val make_properties: Properties.T -> XML.body
    1.23 -  val dest_properties: XML.body -> Properties.T
    1.24 -  val make_string: string -> XML.body
    1.25 -  val dest_string : XML.body -> string
    1.26 -  val make_int: int -> XML.body
    1.27 -  val dest_int : XML.body -> int
    1.28 -  val make_bool: bool -> XML.body
    1.29 -  val dest_bool: XML.body -> bool
    1.30 -  val make_unit: unit -> XML.body
    1.31 -  val dest_unit: XML.body -> unit
    1.32 -  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    1.33 -  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    1.34 -  val make_triple:
    1.35 -    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    1.36 -  val dest_triple:
    1.37 -    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    1.38 -  val make_list: ('a -> XML.body) -> 'a list -> XML.body
    1.39 -  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
    1.40 -  val make_option: ('a -> XML.body) -> 'a option -> XML.body
    1.41 -  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
    1.42 -  val make_variant: ('a -> XML.body) list -> 'a -> XML.body
    1.43 -  val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a
    1.44 +  structure Dest:
    1.45 +  sig
    1.46 +    val properties: XML.body -> Properties.T
    1.47 +    val string : XML.body -> string
    1.48 +    val int : XML.body -> int
    1.49 +    val bool: XML.body -> bool
    1.50 +    val unit: XML.body -> unit
    1.51 +    val pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    1.52 +    val triple: (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    1.53 +    val list: (XML.body -> 'a) -> XML.body -> 'a list
    1.54 +    val option: (XML.body -> 'a) -> XML.body -> 'a option
    1.55 +    val variant: (XML.body -> 'a) list -> XML.body -> 'a
    1.56 +  end
    1.57  end;
    1.58  
    1.59  structure XML_Data: XML_DATA =
    1.60  struct
    1.61  
    1.62 +(** make **)
    1.63 +
    1.64 +structure Make =
    1.65 +struct
    1.66 +
    1.67  (* basic values *)
    1.68  
    1.69 -exception XML_ATOM of string;
    1.70 -
    1.71 -
    1.72 -fun make_int_atom i = signed_string_of_int i;
    1.73 -
    1.74 -fun dest_int_atom s =
    1.75 -  (case Int.fromString s of
    1.76 -    SOME i => i
    1.77 -  | NONE => raise XML_ATOM s);
    1.78 -
    1.79 +fun int_atom i = signed_string_of_int i;
    1.80  
    1.81 -fun make_bool_atom false = "0"
    1.82 -  | make_bool_atom true = "1";
    1.83 +fun bool_atom false = "0"
    1.84 +  | bool_atom true = "1";
    1.85  
    1.86 -fun dest_bool_atom "0" = false
    1.87 -  | dest_bool_atom "1" = true
    1.88 -  | dest_bool_atom s = raise XML_ATOM s;
    1.89 -
    1.90 -
    1.91 -fun make_unit_atom () = "";
    1.92 -
    1.93 -fun dest_unit_atom "" = ()
    1.94 -  | dest_unit_atom s = raise XML_ATOM s;
    1.95 +fun unit_atom () = "";
    1.96  
    1.97  
    1.98  (* structural nodes *)
    1.99  
   1.100 -exception XML_BODY of XML.tree list;
   1.101 -
   1.102 -fun make_node ts = XML.Elem ((":", []), ts);
   1.103 +fun node ts = XML.Elem ((":", []), ts);
   1.104  
   1.105 -fun dest_node (XML.Elem ((":", []), ts)) = ts
   1.106 -  | dest_node t = raise XML_BODY [t];
   1.107 -
   1.108 -fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
   1.109 -
   1.110 -fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
   1.111 -  | dest_tagged t = raise XML_BODY [t];
   1.112 +fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
   1.113  
   1.114  
   1.115  (* representation of standard types *)
   1.116  
   1.117 -fun make_properties props = [XML.Elem ((":", props), [])];
   1.118 -
   1.119 -fun dest_properties [XML.Elem ((":", props), [])] = props
   1.120 -  | dest_properties ts = raise XML_BODY ts;
   1.121 -
   1.122 +fun properties props = [XML.Elem ((":", props), [])];
   1.123  
   1.124 -fun make_string "" = []
   1.125 -  | make_string s = [XML.Text s];
   1.126 -
   1.127 -fun dest_string [] = ""
   1.128 -  | dest_string [XML.Text s] = s
   1.129 -  | dest_string ts = raise XML_BODY ts;
   1.130 -
   1.131 +fun string "" = []
   1.132 +  | string s = [XML.Text s];
   1.133  
   1.134 -val make_int = make_string o make_int_atom;
   1.135 -val dest_int = dest_int_atom o dest_string;
   1.136 -
   1.137 -val make_bool = make_string o make_bool_atom;
   1.138 -val dest_bool = dest_bool_atom o dest_string;
   1.139 +val int = string o int_atom;
   1.140  
   1.141 -val make_unit = make_string o make_unit_atom;
   1.142 -val dest_unit = dest_unit_atom o dest_string;
   1.143 -
   1.144 +val bool = string o bool_atom;
   1.145  
   1.146 -fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
   1.147 -
   1.148 -fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
   1.149 -  | dest_pair _ _ ts = raise XML_BODY ts;
   1.150 +val unit = string o unit_atom;
   1.151  
   1.152 -
   1.153 -fun make_triple make1 make2 make3 (x, y, z) =
   1.154 -  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
   1.155 +fun pair f g (x, y) = [node (f x), node (g y)];
   1.156  
   1.157 -fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
   1.158 -      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
   1.159 -  | dest_triple _ _ _ ts = raise XML_BODY ts;
   1.160 -
   1.161 -
   1.162 -fun make_list make xs = map (make_node o make) xs;
   1.163 -
   1.164 -fun dest_list dest ts = map (dest o dest_node) ts;
   1.165 -
   1.166 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
   1.167  
   1.168 -fun make_option _ NONE = []
   1.169 -  | make_option make (SOME x) = [make_node (make x)];
   1.170 -
   1.171 -fun dest_option _ [] = NONE
   1.172 -  | dest_option dest [t] = SOME (dest (dest_node t))
   1.173 -  | dest_option _ ts = raise XML_BODY ts;
   1.174 -
   1.175 +fun list f xs = map (node o f) xs;
   1.176  
   1.177 -fun make_variant makes x =
   1.178 -  [make_tagged (the (get_index (fn make => try make x) makes))];
   1.179 +fun option _ NONE = []
   1.180 +  | option f (SOME x) = [node (f x)];
   1.181  
   1.182 -fun dest_variant dests [t] =
   1.183 -      let val (tag, ts) = dest_tagged t
   1.184 -      in nth dests tag ts end
   1.185 -  | dest_variant _ ts = raise XML_BODY ts;
   1.186 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
   1.187  
   1.188  end;
   1.189  
   1.190 +
   1.191 +
   1.192 +(** dest **)
   1.193 +
   1.194 +exception XML_ATOM of string;
   1.195 +exception XML_BODY of XML.tree list;
   1.196 +
   1.197 +structure Dest =
   1.198 +struct
   1.199 +
   1.200 +(* basic values *)
   1.201 +
   1.202 +fun int_atom s =
   1.203 +  (case Int.fromString s of
   1.204 +    SOME i => i
   1.205 +  | NONE => raise XML_ATOM s);
   1.206 +
   1.207 +fun bool_atom "0" = false
   1.208 +  | bool_atom "1" = true
   1.209 +  | bool_atom s = raise XML_ATOM s;
   1.210 +
   1.211 +fun unit_atom "" = ()
   1.212 +  | unit_atom s = raise XML_ATOM s;
   1.213 +
   1.214 +
   1.215 +(* structural nodes *)
   1.216 +
   1.217 +fun node (XML.Elem ((":", []), ts)) = ts
   1.218 +  | node t = raise XML_BODY [t];
   1.219 +
   1.220 +fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
   1.221 +  | tagged t = raise XML_BODY [t];
   1.222 +
   1.223 +
   1.224 +(* representation of standard types *)
   1.225 +
   1.226 +fun properties [XML.Elem ((":", props), [])] = props
   1.227 +  | properties ts = raise XML_BODY ts;
   1.228 +
   1.229 +fun string [] = ""
   1.230 +  | string [XML.Text s] = s
   1.231 +  | string ts = raise XML_BODY ts;
   1.232 +
   1.233 +val int = int_atom o string;
   1.234 +
   1.235 +val bool = bool_atom o string;
   1.236 +
   1.237 +val unit = unit_atom o string;
   1.238 +
   1.239 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
   1.240 +  | pair _ _ ts = raise XML_BODY ts;
   1.241 +
   1.242 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   1.243 +  | triple _ _ _ ts = raise XML_BODY ts;
   1.244 +
   1.245 +fun list f ts = map (f o node) ts;
   1.246 +
   1.247 +fun option _ [] = NONE
   1.248 +  | option f [t] = SOME (f (node t))
   1.249 +  | option _ ts = raise XML_BODY ts;
   1.250 +
   1.251 +fun variant fs [t] = uncurry (nth fs) (tagged t)
   1.252 +  | variant _ ts = raise XML_BODY ts;
   1.253 +
   1.254 +end;
   1.255 +
   1.256 +end;
   1.257 +
     2.1 --- a/src/Pure/General/xml_data.scala	Sun Jul 10 13:00:22 2011 +0200
     2.2 +++ b/src/Pure/General/xml_data.scala	Sun Jul 10 13:51:21 2011 +0200
     2.3 @@ -10,150 +10,162 @@
     2.4  
     2.5  object XML_Data
     2.6  {
     2.7 -  /* basic values */
     2.8 +  /** make **/
     2.9  
    2.10 -  class XML_Atom(s: String) extends Exception(s)
    2.11 -
    2.12 +  object Make
    2.13 +  {
    2.14 +    /* basic values */
    2.15  
    2.16 -  private def make_long_atom(i: Long): String = i.toString
    2.17 +    private def long_atom(i: Long): String = i.toString
    2.18 +
    2.19 +    private def int_atom(i: Int): String = i.toString
    2.20  
    2.21 -  private def dest_long_atom(s: String): Long =
    2.22 -    try { java.lang.Long.parseLong(s) }
    2.23 -    catch { case e: NumberFormatException => throw new XML_Atom(s) }
    2.24 +    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
    2.25 +
    2.26 +    private def unit_atom(u: Unit) = ""
    2.27  
    2.28  
    2.29 -  private def make_int_atom(i: Int): String = i.toString
    2.30 -
    2.31 -  private def dest_int_atom(s: String): Int =
    2.32 -    try { Integer.parseInt(s) }
    2.33 -    catch { case e: NumberFormatException => throw new XML_Atom(s) }
    2.34 -
    2.35 -
    2.36 -  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
    2.37 +    /* structural nodes */
    2.38  
    2.39 -  private def dest_bool_atom(s: String): Boolean =
    2.40 -    if (s == "1") true
    2.41 -    else if (s == "0") false
    2.42 -    else throw new XML_Atom(s)
    2.43 +    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    2.44  
    2.45 -
    2.46 -  private def make_unit_atom(u: Unit) = ""
    2.47 -
    2.48 -  private def dest_unit_atom(s: String): Unit =
    2.49 -    if (s == "") () else throw new XML_Atom(s)
    2.50 +    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
    2.51 +      XML.Elem(Markup(int_atom(tag), Nil), ts)
    2.52  
    2.53  
    2.54 -  /* structural nodes */
    2.55 +    /* representation of standard types */
    2.56  
    2.57 -  class XML_Body(body: XML.Body) extends Exception
    2.58 +    def properties(props: List[(String, String)]): XML.Body =
    2.59 +      List(XML.Elem(Markup(":", props), Nil))
    2.60  
    2.61 -  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    2.62 +    def string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
    2.63 +
    2.64 +    def long(i: Long): XML.Body = string(long_atom(i))
    2.65  
    2.66 -  private def dest_node(t: XML.Tree): XML.Body =
    2.67 -    t match {
    2.68 -      case XML.Elem(Markup(":", Nil), ts) => ts
    2.69 -      case _ => throw new XML_Body(List(t))
    2.70 -    }
    2.71 +    def int(i: Int): XML.Body = string(int_atom(i))
    2.72 +
    2.73 +    def bool(b: Boolean): XML.Body = string(bool_atom(b))
    2.74  
    2.75 -  private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
    2.76 -    XML.Elem(Markup(make_int_atom(tag), Nil), ts)
    2.77 +    def unit(u: Unit): XML.Body = string(unit_atom(u))
    2.78 +
    2.79 +    def pair[A, B](f: A => XML.Body, g: B => XML.Body)(p: (A, B)): XML.Body =
    2.80 +      List(node(f(p._1)), node(g(p._2)))
    2.81  
    2.82 -  private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
    2.83 -    t match {
    2.84 -      case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
    2.85 -      case _ => throw new XML_Body(List(t))
    2.86 -    }
    2.87 +    def triple[A, B, C](f: A => XML.Body, g: B => XML.Body, h: C => XML.Body)
    2.88 +        (p: (A, B, C)): XML.Body =
    2.89 +      List(node(f(p._1)), node(g(p._2)), node(h(p._3)))
    2.90  
    2.91 -
    2.92 -  /* representation of standard types */
    2.93 +    def list[A](f: A => XML.Body)(xs: List[A]): XML.Body =
    2.94 +      xs.map((x: A) => node(f(x)))
    2.95  
    2.96 -  def make_properties(props: List[(String, String)]): XML.Body =
    2.97 -    List(XML.Elem(Markup(":", props), Nil))
    2.98 +    def option[A](f: A => XML.Body)(opt: Option[A]): XML.Body =
    2.99 +      opt match {
   2.100 +        case None => Nil
   2.101 +        case Some(x) => List(node(f(x)))
   2.102 +      }
   2.103  
   2.104 -  def dest_properties(ts: XML.Body): List[(String, String)] =
   2.105 -    ts match {
   2.106 -      case List(XML.Elem(Markup(":", props), Nil)) => props
   2.107 -      case _ => throw new XML_Body(ts)
   2.108 +    def variant[A](fs: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
   2.109 +    {
   2.110 +      val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   2.111 +      List(tagged(tag, f(x)))
   2.112      }
   2.113 +  }
   2.114 +
   2.115  
   2.116  
   2.117 -  def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
   2.118 +  /** dest **/
   2.119 +
   2.120 +  class XML_Atom(s: String) extends Exception(s)
   2.121 +  class XML_Body(body: XML.Body) extends Exception
   2.122 +
   2.123 +  object Dest
   2.124 +  {
   2.125 +     /* basic values */
   2.126  
   2.127 -  def dest_string(ts: XML.Body): String =
   2.128 -    ts match {
   2.129 -      case Nil => ""
   2.130 -      case List(XML.Text(s)) => s
   2.131 -      case _ => throw new XML_Body(ts)
   2.132 -    }
   2.133 +    private def long_atom(s: String): Long =
   2.134 +      try { java.lang.Long.parseLong(s) }
   2.135 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   2.136 +
   2.137 +    private def int_atom(s: String): Int =
   2.138 +      try { Integer.parseInt(s) }
   2.139 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   2.140 +
   2.141 +    private def bool_atom(s: String): Boolean =
   2.142 +      if (s == "1") true
   2.143 +      else if (s == "0") false
   2.144 +      else throw new XML_Atom(s)
   2.145 +
   2.146 +    private def unit_atom(s: String): Unit =
   2.147 +      if (s == "") () else throw new XML_Atom(s)
   2.148  
   2.149  
   2.150 -  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
   2.151 -  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
   2.152 -
   2.153 -  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
   2.154 -  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
   2.155 -
   2.156 -  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
   2.157 -  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
   2.158 +    /* structural nodes */
   2.159  
   2.160 -  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
   2.161 -  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
   2.162 -
   2.163 +    private def node(t: XML.Tree): XML.Body =
   2.164 +      t match {
   2.165 +        case XML.Elem(Markup(":", Nil), ts) => ts
   2.166 +        case _ => throw new XML_Body(List(t))
   2.167 +      }
   2.168  
   2.169 -  def make_pair[A, B](make1: A => XML.Body, make2: B => XML.Body)(p: (A, B)): XML.Body =
   2.170 -    List(make_node(make1(p._1)), make_node(make2(p._2)))
   2.171 -
   2.172 -  def dest_pair[A, B](dest1: XML.Body => A, dest2: XML.Body => B)(ts: XML.Body): (A, B) =
   2.173 -    ts match {
   2.174 -      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
   2.175 -      case _ => throw new XML_Body(ts)
   2.176 -    }
   2.177 +    private def tagged(t: XML.Tree): (Int, XML.Body) =
   2.178 +      t match {
   2.179 +        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
   2.180 +        case _ => throw new XML_Body(List(t))
   2.181 +      }
   2.182  
   2.183  
   2.184 -  def make_triple[A, B, C](make1: A => XML.Body, make2: B => XML.Body, make3: C => XML.Body)
   2.185 -      (p: (A, B, C)): XML.Body =
   2.186 -    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
   2.187 +    /* representation of standard types */
   2.188 +
   2.189 +    def properties(ts: XML.Body): List[(String, String)] =
   2.190 +      ts match {
   2.191 +        case List(XML.Elem(Markup(":", props), Nil)) => props
   2.192 +        case _ => throw new XML_Body(ts)
   2.193 +      }
   2.194  
   2.195 -  def dest_triple[A, B, C](dest1: XML.Body => A, dest2: XML.Body => B, dest3: XML.Body => C)
   2.196 -      (ts: XML.Body): (A, B, C) =
   2.197 -    ts match {
   2.198 -      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
   2.199 -      case _ => throw new XML_Body(ts)
   2.200 -    }
   2.201 +    def string(ts: XML.Body): String =
   2.202 +      ts match {
   2.203 +        case Nil => ""
   2.204 +        case List(XML.Text(s)) => s
   2.205 +        case _ => throw new XML_Body(ts)
   2.206 +      }
   2.207  
   2.208 +    def long(ts: XML.Body): Long = long_atom(string(ts))
   2.209  
   2.210 -  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
   2.211 -    xs.map((x: A) => make_node(make(x)))
   2.212 +    def int(ts: XML.Body): Int = int_atom(string(ts))
   2.213  
   2.214 -  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
   2.215 -    ts.map((t: XML.Tree) => dest(dest_node(t)))
   2.216 +    def bool(ts: XML.Body) = bool_atom(string(ts))
   2.217  
   2.218 +    def unit(ts: XML.Body): Unit = unit_atom(string(ts))
   2.219  
   2.220 -  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
   2.221 -    opt match {
   2.222 -      case None => Nil
   2.223 -      case Some(x) => List(make_node(make(x)))
   2.224 -    }
   2.225 +    def pair[A, B](f: XML.Body => A, g: XML.Body => B)(ts: XML.Body): (A, B) =
   2.226 +      ts match {
   2.227 +        case List(t1, t2) => (f(node(t1)), g(node(t2)))
   2.228 +        case _ => throw new XML_Body(ts)
   2.229 +      }
   2.230  
   2.231 -  def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
   2.232 -    ts match {
   2.233 -      case Nil => None
   2.234 -      case List(t) => Some(dest(dest_node(t)))
   2.235 -      case _ => throw new XML_Body(ts)
   2.236 -    }
   2.237 +    def triple[A, B, C](f: XML.Body => A, g: XML.Body => B, h: XML.Body => C)
   2.238 +        (ts: XML.Body): (A, B, C) =
   2.239 +      ts match {
   2.240 +        case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   2.241 +        case _ => throw new XML_Body(ts)
   2.242 +      }
   2.243  
   2.244 +    def list[A](f: XML.Body => A)(ts: XML.Body): List[A] =
   2.245 +      ts.map((t: XML.Tree) => f(node(t)))
   2.246  
   2.247 -  def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
   2.248 -  {
   2.249 -    val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   2.250 -    List(make_tagged(tag, make(x)))
   2.251 -  }
   2.252 +    def option[A](f: XML.Body => A)(ts: XML.Body): Option[A] =
   2.253 +      ts match {
   2.254 +        case Nil => None
   2.255 +        case List(t) => Some(f(node(t)))
   2.256 +        case _ => throw new XML_Body(ts)
   2.257 +      }
   2.258  
   2.259 -  def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
   2.260 -    ts match {
   2.261 -      case List(t) =>
   2.262 -        val (tag, ts) = dest_tagged(t)
   2.263 -        dests(tag)(ts)
   2.264 -      case _ => throw new XML_Body(ts)
   2.265 -    }
   2.266 +    def variant[A](fs: List[XML.Body => A])(ts: XML.Body): A =
   2.267 +      ts match {
   2.268 +        case List(t) =>
   2.269 +          val (tag, ts) = tagged(t)
   2.270 +          fs(tag)(ts)
   2.271 +        case _ => throw new XML_Body(ts)
   2.272 +      }
   2.273 +  }
   2.274  }
     3.1 --- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 13:00:22 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 13:51:21 2011 +0200
     3.3 @@ -17,21 +17,12 @@
     3.4        let
     3.5          val old_id = Document.parse_id old_id_string;
     3.6          val new_id = Document.parse_id new_id_string;
     3.7 -        val edits =
     3.8 -          XML_Data.dest_list
     3.9 -            (XML_Data.dest_pair
    3.10 -              XML_Data.dest_string
    3.11 -              (XML_Data.dest_option
    3.12 -                (XML_Data.dest_list
    3.13 -                  (XML_Data.dest_pair
    3.14 -                    (XML_Data.dest_option XML_Data.dest_int)
    3.15 -                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    3.16 -        val headers =
    3.17 -          XML_Data.dest_list
    3.18 -            (XML_Data.dest_pair XML_Data.dest_string
    3.19 -              (XML_Data.dest_triple XML_Data.dest_string
    3.20 -                (XML_Data.dest_list XML_Data.dest_string)
    3.21 -                (XML_Data.dest_list XML_Data.dest_string))) (YXML.parse_body headers_yxml);
    3.22 +        val edits = YXML.parse_body edits_yxml |>
    3.23 +          let open XML_Data.Dest
    3.24 +          in list (pair string (option (list (pair (option int) (option int))))) end;
    3.25 +        val headers = YXML.parse_body headers_yxml |>
    3.26 +          let open XML_Data.Dest
    3.27 +          in list (pair string (triple string (list string) (list string))) end;
    3.28  
    3.29        val await_cancellation = Document.cancel_execution state;
    3.30        val (updates, state') = Document.edit old_id new_id edits headers state;
     4.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:00:22 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:51:21 2011 +0200
     4.3 @@ -143,15 +143,12 @@
     4.4        edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
     4.5    {
     4.6      val arg1 =
     4.7 -      XML_Data.make_list(
     4.8 -        XML_Data.make_pair(XML_Data.make_string,
     4.9 -          XML_Data.make_option(XML_Data.make_list(
    4.10 -              XML_Data.make_pair(
    4.11 -                XML_Data.make_option(XML_Data.make_long),
    4.12 -                XML_Data.make_option(XML_Data.make_long))))))(edits)
    4.13 +    { import XML_Data.Make._
    4.14 +      list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
    4.15  
    4.16      val arg2 =
    4.17 -      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
    4.18 +    { import XML_Data.Make._
    4.19 +      list(pair(string, Thy_Header.make_xml_data))(headers) }
    4.20  
    4.21      input("Isar_Document.edit_version",
    4.22        Document.ID(old_id), Document.ID(new_id),
     5.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:00:22 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:51:21 2011 +0200
     5.3 @@ -32,9 +32,8 @@
     5.4    }
     5.5  
     5.6    def make_xml_data(header: Header): XML.Body =
     5.7 -    XML_Data.make_triple(XML_Data.make_string,
     5.8 -      XML_Data.make_list(XML_Data.make_string),
     5.9 -        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
    5.10 +  { import XML_Data.Make._
    5.11 +    triple(string, list(string), list(string))(header.name, header.imports, header.uses) }
    5.12  
    5.13  
    5.14    /* file name */
     6.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 13:00:22 2011 +0200
     6.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 13:51:21 2011 +0200
     6.3 @@ -139,8 +139,8 @@
     6.4            |> (if rem_dups then cons ("rem_dups", "") else I)
     6.5            |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
     6.6        in
     6.7 -        XML.Elem (("Query", properties), XML_Data.make_list 
     6.8 -          (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
     6.9 +        XML.Elem (("Query", properties), XML_Data.Make.list
    6.10 +          (XML_Data.Make.pair XML_Data.Make.bool (single o xml_of_criterion)) criteria)
    6.11        end
    6.12    | xml_of_query _ = raise Fail "cannot serialize goal";
    6.13  
    6.14 @@ -148,8 +148,9 @@
    6.15        let
    6.16          val rem_dups = Properties.defined properties "rem_dups";
    6.17          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
    6.18 -        val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool 
    6.19 -          (criterion_of_xml o the_single)) body;
    6.20 +        val criteria =
    6.21 +          XML_Data.Dest.list (XML_Data.Dest.pair XML_Data.Dest.bool 
    6.22 +            (criterion_of_xml o the_single)) body;
    6.23        in
    6.24          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
    6.25        end
    6.26 @@ -189,12 +190,12 @@
    6.27      val properties =
    6.28        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
    6.29    in
    6.30 -    XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
    6.31 +    XML.Elem (("Result", properties), XML_Data.Make.list (single o xml_of_theorem) theorems)
    6.32    end;
    6.33  
    6.34  fun result_of_xml (XML.Elem (("Result", properties), body)) =
    6.35        (Properties.get properties "found" |> Option.map Markup.parse_int,
    6.36 -       XML_Data.dest_list (theorem_of_xml o the_single) body)
    6.37 +       XML_Data.Dest.list (theorem_of_xml o the_single) body)
    6.38    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
    6.39  
    6.40  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm