# HG changeset patch
# User wenzelm
# Date 1490020634 -3600
# Node ID 289561ca4fa3ecc4e6713636be0b3bef245bfe05
# Parent  7dbb780f24a9b682926e9f9193423110f63e7767
more operations;

diff -r 7dbb780f24a9 -r 289561ca4fa3 src/Pure/PIDE/xml.ML
--- 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;
 
diff -r 7dbb780f24a9 -r 289561ca4fa3 src/Pure/PIDE/xml.scala
--- 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