src/Pure/PIDE/yxml.scala

--- a/src/Pure/PIDE/yxml.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/PIDE/yxml.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -18,6 +18,10 @@
 
   val X = '\5'
   val Y = '\6'
+
+  val is_X = (c: Char) => c == X
+  val is_Y = (c: Char) => c == Y
+
   val X_string = X.toString
   val Y_string = Y.toString
 
@@ -93,10 +97,10 @@
 
     /* parse chunks */
 
-    for (chunk <- Library.separated_chunks(X, source) if chunk.length != 0) {
+    for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) {
       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
-        Library.separated_chunks(Y, chunk).toList match {
+        Library.separated_chunks(is_Y, chunk).toList match {
           case ch :: name :: atts if ch.length == 0 =>
             push(name.toString, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))