src/Pure/PIDE/yxml.scala
changeset 73556 192bcee4f8b8
parent 73340 0ffcad1f6130
child 73712 3eba8d4b624b
--- 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)