--- a/src/Pure/PIDE/xml.ML Mon Mar 20 14:36:15 2017 +0100
+++ b/src/Pure/PIDE/xml.ML Mon Mar 20 15:37:14 2017 +0100
@@ -52,8 +52,16 @@
val parse: string -> tree
exception XML_ATOM of string
exception XML_BODY of body
- structure Encode: XML_DATA_OPS
- structure Decode: XML_DATA_OPS
+ structure Encode:
+ sig
+ include XML_DATA_OPS
+ val tree: tree T
+ end
+ structure Decode:
+ sig
+ include XML_DATA_OPS
+ val tree: tree T
+ end
end;
structure XML: XML =
@@ -302,6 +310,8 @@
(* representation of standard types *)
+fun tree (t: tree) = [t];
+
fun properties props = [Elem ((":", props), [])];
fun string "" = []
@@ -364,6 +374,9 @@
(* representation of standard types *)
+fun tree [t] = t
+ | tree ts = raise XML_BODY ts;
+
fun properties [Elem ((":", props), [])] = props
| properties ts = raise XML_BODY ts;