--- a/src/Pure/General/yxml.scala Thu Aug 21 21:27:07 2008 +0200
+++ b/src/Pure/General/yxml.scala Thu Aug 21 21:42:16 2008 +0200
@@ -16,6 +16,7 @@
private val X = '\5'
private val Y = '\6'
+ private val Y_string = Y.toString
def detect(source: CharSequence) = {
source.length >= 2 &&
@@ -89,10 +90,12 @@
stack = List((("", Nil), Nil))
for (chunk <- chunks(X, source) if chunk != "") {
- chunks(Y, chunk).toList match {
- case List("", "") => pop()
- case "" :: name :: atts => push(name.toString, atts.map(parse_attrib))
- case txts => for (txt <- txts) add(XML.Text(txt.toString))
+ if (chunk == Y_string) pop()
+ else {
+ chunks(Y, chunk).toList match {
+ case "" :: name :: atts => push(name.toString, atts.map(parse_attrib))
+ case txts => for (txt <- txts) add(XML.Text(txt.toString))
+ }
}
}
stack match {