diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/General/xml_data.ML
--- a/src/Pure/General/xml_data.ML	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/General/xml_data.ML	Sun Jul 10 13:51:21 2011 +0200
@@ -6,137 +6,152 @@
 
 signature XML_DATA =
 sig
+  structure Make:
+  sig
+    val properties: Properties.T -> XML.body
+    val string: string -> XML.body
+    val int: int -> XML.body
+    val bool: bool -> XML.body
+    val unit: unit -> XML.body
+    val pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
+    val triple: ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
+    val list: ('a -> XML.body) -> 'a list -> XML.body
+    val option: ('a -> XML.body) -> 'a option -> XML.body
+    val variant: ('a -> XML.body) list -> 'a -> XML.body
+  end
   exception XML_ATOM of string
   exception XML_BODY of XML.body
-  val make_properties: Properties.T -> XML.body
-  val dest_properties: XML.body -> Properties.T
-  val make_string: string -> XML.body
-  val dest_string : XML.body -> string
-  val make_int: int -> XML.body
-  val dest_int : XML.body -> int
-  val make_bool: bool -> XML.body
-  val dest_bool: XML.body -> bool
-  val make_unit: unit -> XML.body
-  val dest_unit: XML.body -> unit
-  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
-  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
-  val make_triple:
-    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
-  val dest_triple:
-    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
-  val make_list: ('a -> XML.body) -> 'a list -> XML.body
-  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
+  structure Dest:
+  sig
+    val properties: XML.body -> Properties.T
+    val string : XML.body -> string
+    val int : XML.body -> int
+    val bool: XML.body -> bool
+    val unit: XML.body -> unit
+    val pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
+    val triple: (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
+    val list: (XML.body -> 'a) -> XML.body -> 'a list
+    val option: (XML.body -> 'a) -> XML.body -> 'a option
+    val variant: (XML.body -> 'a) list -> XML.body -> 'a
+  end
 end;
 
 structure XML_Data: XML_DATA =
 struct
 
+(** make **)
+
+structure Make =
+struct
+
 (* basic values *)
 
-exception XML_ATOM of string;
-
-
-fun make_int_atom i = signed_string_of_int i;
-
-fun dest_int_atom s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise XML_ATOM s);
-
+fun int_atom i = signed_string_of_int i;
 
-fun make_bool_atom false = "0"
-  | make_bool_atom true = "1";
+fun bool_atom false = "0"
+  | bool_atom true = "1";
 
-fun dest_bool_atom "0" = false
-  | dest_bool_atom "1" = true
-  | dest_bool_atom s = raise XML_ATOM s;
-
-
-fun make_unit_atom () = "";
-
-fun dest_unit_atom "" = ()
-  | dest_unit_atom s = raise XML_ATOM s;
+fun unit_atom () = "";
 
 
 (* structural nodes *)
 
-exception XML_BODY of XML.tree list;
-
-fun make_node ts = XML.Elem ((":", []), ts);
+fun node ts = XML.Elem ((":", []), ts);
 
-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];
+fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
 
 
 (* representation of standard types *)
 
-fun make_properties props = [XML.Elem ((":", props), [])];
-
-fun dest_properties [XML.Elem ((":", props), [])] = props
-  | dest_properties ts = raise XML_BODY ts;
-
+fun properties props = [XML.Elem ((":", props), [])];
 
-fun make_string "" = []
-  | make_string s = [XML.Text s];
-
-fun dest_string [] = ""
-  | dest_string [XML.Text s] = s
-  | dest_string ts = raise XML_BODY ts;
-
+fun string "" = []
+  | string s = [XML.Text s];
 
-val make_int = make_string o make_int_atom;
-val dest_int = dest_int_atom o dest_string;
-
-val make_bool = make_string o make_bool_atom;
-val dest_bool = dest_bool_atom o dest_string;
+val int = string o int_atom;
 
-val make_unit = make_string o make_unit_atom;
-val dest_unit = dest_unit_atom o dest_string;
-
+val bool = string o bool_atom;
 
-fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
-
-fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
-  | dest_pair _ _ ts = raise XML_BODY ts;
+val unit = string o unit_atom;
 
-
-fun make_triple make1 make2 make3 (x, y, z) =
-  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
+fun pair f g (x, y) = [node (f x), node (g y)];
 
-fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
-      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
-  | dest_triple _ _ _ ts = raise XML_BODY ts;
-
-
-fun make_list make xs = map (make_node o make) xs;
-
-fun dest_list dest ts = map (dest o dest_node) ts;
-
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
 
-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 list f xs = map (node o f) xs;
 
-fun make_variant makes x =
-  [make_tagged (the (get_index (fn make => try make x) makes))];
+fun option _ NONE = []
+  | option f (SOME x) = [node (f x)];
 
-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;
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
 
 end;
 
+
+
+(** dest **)
+
+exception XML_ATOM of string;
+exception XML_BODY of XML.tree list;
+
+structure Dest =
+struct
+
+(* 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;
+