diff -r 437895863e1d -r d55cdb87f332 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Sun Jul 14 15:49:26 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Sun Jul 14 15:50:42 2024 +0200
@@ -148,14 +148,16 @@
 
     /* parse chunks */
 
-    for (chunk <- source.iterator_X if !chunk.is_empty) {
-      if (chunk.is_Y) pop()
-      else {
-        chunk.iterator_Y.toList match {
-          case ch :: name :: atts if ch.is_empty =>
-            push(parse_string(name), atts.map(parse_attrib))
-          case txts =>
-            for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
+    for (chunk <- source.iterator_X) {
+      if (!chunk.is_empty) {
+        if (chunk.is_Y) pop()
+        else {
+          chunk.iterator_Y.toList match {
+            case ch :: name :: atts if ch.is_empty =>
+              push(parse_string(name), atts.map(parse_attrib))
+            case txts =>
+              for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
+          }
         }
       }
     }