--- a/src/Pure/PIDE/xml.ML Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/PIDE/xml.ML Sat Nov 02 12:02:27 2019 +0100
@@ -34,6 +34,7 @@
Elem of (string * attributes) * tree list
| Text of string
type body = tree list
+ val blob: string list -> body
val xml_elemN: string
val xml_nameN: string
val xml_bodyN: string
@@ -73,13 +74,9 @@
(** XML trees **)
-type attributes = (string * string) list;
+open Output_Primitives.XML;
-datatype tree =
- Elem of (string * attributes) * tree list
- | Text of string;
-
-type body = tree list;
+val blob = map Text;
(* wrapped elements *)