--- 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;
--- a/src/Pure/PIDE/xml.scala Mon Mar 20 14:36:15 2017 +0100
+++ b/src/Pure/PIDE/xml.scala Mon Mar 20 15:37:14 2017 +0100
@@ -240,6 +240,8 @@
/* representation of standard types */
+ val tree: T[XML.Tree] = (t => List(t))
+
val properties: T[Properties.T] =
(props => List(XML.Elem(Markup(":", props), Nil)))
@@ -322,6 +324,12 @@
/* representation of standard types */
+ val tree: T[XML.Tree] =
+ {
+ case List(t) => t
+ case ts => throw new XML_Body(ts)
+ }
+
val properties: T[Properties.T] =
{
case List(XML.Elem(Markup(":", props), Nil)) => props