# HG changeset patch
# User wenzelm
# Date 1618084259 -7200
# Node ID 192bcee4f8b856e4f534bf218969fd8d1f48dfe4
# Parent  c973b530002512437cc79109b10d1ab54d4cbd51
more robust treatment of empty markup: it allows to produce formal chunks;

diff -r c973b5300025 -r 192bcee4f8b8 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Apr 10 21:50:59 2021 +0200
@@ -727,6 +727,8 @@
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
+  def is_empty: Boolean = name.isEmpty
+
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
diff -r c973b5300025 -r 192bcee4f8b8 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;
 
diff -r c973b5300025 -r 192bcee4f8b8 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sat Apr 10 21:50:59 2021 +0200
@@ -68,10 +68,12 @@
 fun traverse string =
   let
     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
-    fun tree (XML.Elem ((name, atts), ts)) =
-          string XY #> string name #> fold attrib atts #> string X #>
-          fold tree ts #>
-          string XYX
+    fun tree (XML.Elem (markup as (name, atts), ts)) =
+          if Markup.is_empty markup then fold tree ts
+          else
+            string XY #> string name #> fold attrib atts #> string X #>
+            fold tree ts #>
+            string XYX
       | tree (XML.Text s) = string s;
   in tree end;
 
diff -r c973b5300025 -r 192bcee4f8b8 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/Pure/PIDE/yxml.scala	Sat Apr 10 21:50:59 2021 +0200
@@ -36,13 +36,16 @@
   {
     def tree(t: XML.Tree): Unit =
       t match {
-        case XML.Elem(Markup(name, atts), ts) =>
-          string(XY_string)
-          string(name)
-          for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
-          string(X_string)
-          ts.foreach(tree)
-          string(XYX_string)
+        case XML.Elem(markup @ Markup(name, atts), ts) =>
+          if (markup.is_empty) ts.foreach(tree)
+          else {
+            string(XY_string)
+            string(name)
+            for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
+            string(X_string)
+            ts.foreach(tree)
+            string(XYX_string)
+          }
         case XML.Text(text) => string(text)
       }
     body.foreach(tree)