src/Pure/PIDE/xml.ML

--- a/src/Pure/PIDE/xml.ML	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/Pure/PIDE/xml.ML	Sat Apr 10 21:50:59 2021 +0200
@@ -35,6 +35,7 @@
     | Text of string
   type body = tree list
   val blob: string list -> body
+  val chunk: body -> tree
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
   val xml_elemN: string
@@ -79,6 +80,8 @@
 
 val blob = map Text;
 
+fun chunk body = Elem (Markup.empty, body);
+
 fun is_empty (Text "") = true
   | is_empty _ = false;