# HG changeset patch
# User wenzelm
# Date 1219346827 -7200
# Node ID 2bf3f30558edfe7245692e3a09ce70c7f05abc4f
# Parent  f34ff5e7728fd483d9b93ccb7cd717de632bed2b
parse_attrib: more efficient due to indexOf('=');

diff -r f34ff5e7728f -r 2bf3f30558ed src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu Aug 21 20:53:31 2008 +0200
+++ b/src/Pure/General/yxml.scala	Thu Aug 21 21:27:07 2008 +0200
@@ -56,12 +56,12 @@
     if (name == "") err("unbalanced element")
     else err("unbalanced element \"" + name + "\"")
 
-  private def parse_attrib(s: CharSequence) =
-    chunks('=', s).toList match {
-      case Nil => err_attribute()
-      case "" :: _ => err_attribute()
-      case a :: xs => (a.toString, xs.mkString("="))
-    }
+  private def parse_attrib(source: CharSequence) = {
+    val s = source.toString
+    val i = s.indexOf('=')
+    if (i <= 0) err_attribute()
+    (s.substring(0, i - 1), s.substring(i + 1))
+  }
 
 
   def parse_body(source: CharSequence) = {