1.1 --- a/src/Pure/General/xml_data.ML	Thu Jul 07 22:04:30 2011 +0200
     1.2 +++ b/src/Pure/General/xml_data.ML	Thu Jul 07 23:55:15 2011 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4    val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
     1.5    val make_option: ('a -> XML.body) -> 'a option -> XML.body
     1.6    val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
     1.7 +  val make_variant: ('a -> XML.body) list -> 'a -> XML.body
     1.8 +  val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a
     1.9  end;
    1.10  
    1.11  structure XML_Data: XML_DATA =
    1.12 @@ -69,6 +71,11 @@
    1.13  fun dest_node (XML.Elem ((":", []), ts)) = ts
    1.14    | dest_node t = raise XML_BODY [t];
    1.15  
    1.16 +fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
    1.17 +
    1.18 +fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
    1.19 +  | dest_tagged t = raise XML_BODY [t];
    1.20 +
    1.21  
    1.22  (* representation of standard types *)
    1.23  
    1.24 @@ -115,14 +122,21 @@
    1.25  fun dest_list dest ts = map (dest o dest_node) ts;
    1.26  
    1.27  
    1.28 -fun make_option make NONE = make_list make []
    1.29 -  | make_option make (SOME x) = make_list make [x];
    1.30 +fun make_option _ NONE = []
    1.31 +  | make_option make (SOME x) = [make_node (make x)];
    1.32  
    1.33 -fun dest_option dest ts =
    1.34 -  (case dest_list dest ts of
    1.35 -    [] => NONE
    1.36 -  | [x] => SOME x
    1.37 -  | _ => raise XML_BODY ts);
    1.38 +fun dest_option _ [] = NONE
    1.39 +  | dest_option dest [t] = SOME (dest (dest_node t))
    1.40 +  | dest_option _ ts = raise XML_BODY ts;
    1.41 +
    1.42 +
    1.43 +fun make_variant makes x =
    1.44 +  [make_tagged (the (get_index (fn make => try make x) makes))];
    1.45 +
    1.46 +fun dest_variant dests [t] =
    1.47 +      let val (tag, ts) = dest_tagged t
    1.48 +      in nth dests tag ts end
    1.49 +  | dest_variant _ ts = raise XML_BODY ts;
    1.50  
    1.51  end;
    1.52  

     2.1 --- a/src/Pure/General/xml_data.scala	Thu Jul 07 22:04:30 2011 +0200
     2.2 +++ b/src/Pure/General/xml_data.scala	Thu Jul 07 23:55:15 2011 +0200
     2.3 @@ -55,6 +55,15 @@
     2.4        case _ => throw new XML_Body(List(t))
     2.5      }
     2.6  
     2.7 +  private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
     2.8 +    XML.Elem(Markup(make_int_atom(tag), Nil), ts)
     2.9 +
    2.10 +  private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
    2.11 +    t match {
    2.12 +      case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
    2.13 +      case _ => throw new XML_Body(List(t))
    2.14 +    }
    2.15 +
    2.16  
    2.17    /* representation of standard types */
    2.18  
    2.19 @@ -122,14 +131,29 @@
    2.20  
    2.21    def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
    2.22      opt match {
    2.23 -      case None => make_list(make)(Nil)
    2.24 -      case Some(x) => make_list(make)(List(x))
    2.25 +      case None => Nil
    2.26 +      case Some(x) => List(make_node(make(x)))
    2.27      }
    2.28  
    2.29    def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
    2.30 -    dest_list(dest)(ts) match {
    2.31 +    ts match {
    2.32        case Nil => None
    2.33 -      case List(x) => Some(x)
    2.34 +      case List(t) => Some(dest(dest_node(t)))
    2.35 +      case _ => throw new XML_Body(ts)
    2.36 +    }
    2.37 +
    2.38 +
    2.39 +  def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
    2.40 +  {
    2.41 +    val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
    2.42 +    List(make_tagged(tag, make(x)))
    2.43 +  }
    2.44 +
    2.45 +  def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
    2.46 +    ts match {
    2.47 +      case List(t) =>
    2.48 +        val (tag, ts) = dest_tagged(t)
    2.49 +        dests(tag)(ts)
    2.50        case _ => throw new XML_Body(ts)
    2.51      }
    2.52  }