src/Pure/library.scala

--- a/src/Pure/library.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/library.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -52,13 +52,13 @@
     result.toList
   }
 
-  def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
+  def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {
       private val end = source.length
       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
       {
         if (i < end) {
-          var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+          var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
           Some((source.subSequence(i + 1, j), j))
         }
         else None
@@ -74,7 +74,7 @@
     }
 
   def space_explode(sep: Char, str: String): List[String] =
-    separated_chunks(sep, str).map(_.toString).toList
+    separated_chunks(_ == sep, str).map(_.toString).toList
 
 
   /* lines */
@@ -91,7 +91,7 @@
 
   def first_line(source: CharSequence): String =
   {
-    val lines = separated_chunks('\n', source)
+    val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next.toString
     else ""
   }