diff -r 5ac9a0f9fad0 -r f34ff5e7728f src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu Aug 21 20:51:41 2008 +0200
+++ b/src/Pure/General/yxml.scala	Thu Aug 21 20:53:31 2008 +0200
@@ -12,7 +12,7 @@
 
 object YXML {
 
-  /* markers */
+  /* chunk markers */
 
   private val X = '\5'
   private val Y = '\6'
@@ -24,6 +24,27 @@
   }
 
 
+  /* iterate over chunks (resembles space_explode in ML) */
+
+  private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {
+    private val end = source.length
+    private var state = if (end == 0) None else get_chunk(-1)
+    private def get_chunk(i: Int) = {
+      if (i < end) {
+        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+        Some((source.subSequence(i + 1, j), j))
+      }
+      else None
+    }
+
+    def hasNext() = state.isDefined
+    def next() = state match {
+      case Some((s, i)) => { state = get_chunk(i); s }
+      case None => throw new NoSuchElementException("next on empty iterator")
+    }
+  }
+
+
   /* parsing */
 
   class BadYXML(msg: String) extends Exception
@@ -35,14 +56,11 @@
     if (name == "") err("unbalanced element")
     else err("unbalanced element \"" + name + "\"")
 
-  private val X_pattern = Pattern.compile(Pattern.quote(X.toString))
-  private val Y_pattern = Pattern.compile(Pattern.quote(Y.toString))
-  private val eq_pattern = Pattern.compile(Pattern.quote("="))
-
-  private def parse_attrib(s: String) =
-    eq_pattern.split(s, 2).toList match {
-      case List(x, y) => if (x != "") (x, y) else err_attribute()
-      case _ => err_attribute()
+  private def parse_attrib(s: CharSequence) =
+    chunks('=', s).toList match {
+      case Nil => err_attribute()
+      case "" :: _ => err_attribute()
+      case a :: xs => (a.toString, xs.mkString("="))
     }
 
 
@@ -70,11 +88,11 @@
     /* parse chunks */
 
     stack = List((("", Nil), Nil))
-    for (chunk <- X_pattern.split(source) if chunk != "") {
-      Y_pattern.split(chunk).toList match {
-        case Nil => pop()
-        case "" :: name :: atts => push(name, atts.map(parse_attrib))
-        case txts => for (txt <- txts) add(XML.Text(txt))
+    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))
       }
     }
     stack match {