src/Pure/library.scala

     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 && !sep(source.charAt(j)))
+          var j = i
+          var cont = true
+          while (cont) {
+            j += 1
+            cont = (j < end && !sep(source.charAt(j)))
+          }
           Some((source.subSequence(i + 1, j), j))
         }
         else None
       }
       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)