# HG changeset patch
# User wenzelm
# Date 1310075715 -7200
# Node ID 91c4d7397f0ed6facf0bc3d4698bb49db0bf222c
# Parent  77ce24aa1770fb21272324aa04b41bdd6b8fa930
simplified make_option/dest_option;
added make_variant/dest_variant -- usual representation of datatypes;

diff -r 77ce24aa1770 -r 91c4d7397f0e src/Pure/General/xml_data.ML
--- a/src/Pure/General/xml_data.ML	Thu Jul 07 22:04:30 2011 +0200
+++ b/src/Pure/General/xml_data.ML	Thu Jul 07 23:55:15 2011 +0200
@@ -28,6 +28,8 @@
   val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
   val make_option: ('a -> XML.body) -> 'a option -> XML.body
   val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
+  val make_variant: ('a -> XML.body) list -> 'a -> XML.body
+  val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a
 end;
 
 structure XML_Data: XML_DATA =
@@ -69,6 +71,11 @@
 fun dest_node (XML.Elem ((":", []), ts)) = ts
   | dest_node t = raise XML_BODY [t];
 
+fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
+
+fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
+  | dest_tagged t = raise XML_BODY [t];
+
 
 (* representation of standard types *)
 
@@ -115,14 +122,21 @@
 fun dest_list dest ts = map (dest o dest_node) ts;
 
 
-fun make_option make NONE = make_list make []
-  | make_option make (SOME x) = make_list make [x];
+fun make_option _ NONE = []
+  | make_option make (SOME x) = [make_node (make x)];
+
+fun dest_option _ [] = NONE
+  | dest_option dest [t] = SOME (dest (dest_node t))
+  | dest_option _ ts = raise XML_BODY ts;
+
 
-fun dest_option dest ts =
-  (case dest_list dest ts of
-    [] => NONE
-  | [x] => SOME x
-  | _ => raise XML_BODY ts);
+fun make_variant makes x =
+  [make_tagged (the (get_index (fn make => try make x) makes))];
+
+fun dest_variant dests [t] =
+      let val (tag, ts) = dest_tagged t
+      in nth dests tag ts end
+  | dest_variant _ ts = raise XML_BODY ts;
 
 end;
 
diff -r 77ce24aa1770 -r 91c4d7397f0e src/Pure/General/xml_data.scala
--- a/src/Pure/General/xml_data.scala	Thu Jul 07 22:04:30 2011 +0200
+++ b/src/Pure/General/xml_data.scala	Thu Jul 07 23:55:15 2011 +0200
@@ -55,6 +55,15 @@
       case _ => throw new XML_Body(List(t))
     }
 
+  private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
+    XML.Elem(Markup(make_int_atom(tag), Nil), ts)
+
+  private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
+    t match {
+      case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
+      case _ => throw new XML_Body(List(t))
+    }
+
 
   /* representation of standard types */
 
@@ -122,14 +131,29 @@
 
   def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
     opt match {
-      case None => make_list(make)(Nil)
-      case Some(x) => make_list(make)(List(x))
+      case None => Nil
+      case Some(x) => List(make_node(make(x)))
     }
 
   def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
-    dest_list(dest)(ts) match {
+    ts match {
       case Nil => None
-      case List(x) => Some(x)
+      case List(t) => Some(dest(dest_node(t)))
+      case _ => throw new XML_Body(ts)
+    }
+
+
+  def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
+  {
+    val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+    List(make_tagged(tag, make(x)))
+  }
+
+  def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
+    ts match {
+      case List(t) =>
+        val (tag, ts) = dest_tagged(t)
+        dests(tag)(ts)
       case _ => throw new XML_Body(ts)
     }
 }