--- 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)))))
+ }
}
}
}