src/Pure/library.scala

--- a/src/Pure/library.scala	Wed Jul 27 12:49:31 2022 +0200
+++ b/src/Pure/library.scala	Wed Jul 27 13:13:59 2022 +0200
@@ -70,11 +70,10 @@
       private def next_chunk(i: Int): Option[(CharSequence, Int)] = {
         if (i < end) {
           var j = i
-          var cont = true
-          while (cont) {
+          while ({
             j += 1
-            cont = (j < end && !sep(source.charAt(j)))
-          }
+            j < end && !sep(source.charAt(j))
+          }) ()
           Some((source.subSequence(i + 1, j), j))
         }
         else None