# HG changeset patch
# User wenzelm
# Date 1219347736 -7200
# Node ID d2dc5a1903e89de2009ab7fd59e69c5950a08b4e
# Parent  2bf3f30558edfe7245692e3a09ce70c7f05abc4f
tuned parse performance: avoid splitting terminal Y chunk;

diff -r 2bf3f30558ed -r d2dc5a1903e8 src/Pure/General/yxml.scala
--- 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 {