clarified treatment of empty markup;

--- a/src/Pure/PIDE/xml.scala	Thu Jun 27 22:39:20 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Jun 27 23:18:28 2024 +0200
@@ -63,8 +63,10 @@
         list match {
           case Nil =>
           case Text(s) :: rest => text(s); trav(rest)
-          case Elem(markup, Nil) :: rest => elem(markup, end = true); trav(rest)
-          case Elem(markup, body) :: rest => elem(markup); trav(body ::: End(markup.name) :: rest)
+          case Elem(markup, body) :: rest =>
+            if (markup.is_empty) trav(body ::: rest)
+            else if (body.isEmpty) { elem(markup, end = true); trav(rest) }
+            else { elem(markup); trav(body ::: End(markup.name) :: rest) }
           case End(name) :: rest => end_elem(name); trav(rest)
           case _ :: _ => ???
         }