# HG changeset patch
# User wenzelm
# Date 1719830223 -7200
# Node ID 38d020af64aa3186ee3f576371d46a0a18ce3742
# Parent  8cd4c7da199ae3572b48c7782f08f7dd4788f06a
tuned signature: more operations;

diff -r 8cd4c7da199a -r 38d020af64aa src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sun Jun 30 13:20:54 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Mon Jul 01 12:37:03 2024 +0200
@@ -15,6 +15,8 @@
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
+  val self: Output_Primitives.XML.body T
+  val tree: Output_Primitives.XML.tree T
   val properties: Properties.T T
   val string: string T
   val int: int T
@@ -60,16 +62,8 @@
   val parse: string -> tree
   exception XML_ATOM of string
   exception XML_BODY of body
-  structure Encode:
-  sig
-    include XML_DATA_OPS
-    val tree: tree T
-  end
-  structure Decode:
-  sig
-    include XML_DATA_OPS
-    val tree: tree T
-  end
+  structure Encode: XML_DATA_OPS
+  structure Decode: XML_DATA_OPS
 end;
 
 structure XML: XML =
@@ -321,6 +315,8 @@
 
 (* representation of standard types *)
 
+fun self (x: body) = x;
+
 fun tree (t: tree) = [t];
 
 fun properties props = [Elem ((":", props), [])];
@@ -386,6 +382,8 @@
 
 (* representation of standard types *)
 
+fun self (x: body) = x;
+
 fun tree [t] = t
   | tree ts = raise XML_BODY ts;
 
diff -r 8cd4c7da199a -r 38d020af64aa src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Jun 30 13:20:54 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Mon Jul 01 12:37:03 2024 +0200
@@ -338,6 +338,8 @@
 
     /* representation of standard types */
 
+    val self: T[XML.Body] = identity
+
     val tree: T[XML.Tree] = (t => List(t))
 
     val properties: T[Properties.T] =
@@ -420,6 +422,8 @@
 
     /* representation of standard types */
 
+    val self: T[XML.Body] = identity
+
     val tree: T[XML.Tree] = {
       case List(t) => t
       case ts => throw new XML_Body(ts)