# HG changeset patch
# User wenzelm
# Date 1658920439 -7200
# Node ID a068fb7346efaf452b3b00ced314dcca2f40d97a
# Parent  0caf8528b07bbc8e561534f5b2595b4c73f29335
clarified while-loops;

diff -r 0caf8528b07b -r a068fb7346ef src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jul 27 12:49:31 2022 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jul 27 13:13:59 2022 +0200
@@ -57,12 +57,11 @@
       val buf = new Array[Byte](8192)
       var m = 0
 
-      var cont = true
-      while (cont) {
+      while ({
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
-        cont = (m != -1 && limit > out.size)
-      }
+        m != -1 && limit > out.size
+      }) ()
 
       new Bytes(out.toByteArray, 0, out.size)
     }
diff -r 0caf8528b07b -r a068fb7346ef src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Wed Jul 27 12:49:31 2022 +0200
+++ b/src/Pure/General/sha1.scala	Wed Jul 27 13:13:59 2022 +0200
@@ -36,12 +36,11 @@
     make_digest(sha => using(new FileInputStream(file)) { stream =>
       val buf = new Array[Byte](65536)
       var m = 0
-      var cont = true
-      while (cont) {
+      while ({
         m = stream.read(buf, 0, buf.length)
         if (m != -1) sha.update(buf, 0, m)
-        cont = (m != -1)
-      }
+        m != -1
+      }) ()
     })
 
   def digest(path: Path): Digest = digest(path.file)
diff -r 0caf8528b07b -r a068fb7346ef src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Jul 27 12:49:31 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Jul 27 13:13:59 2022 +0200
@@ -1136,12 +1136,11 @@
           val buf = ByteBuffer.allocate(n)
           var i = 0
           var m = 0
-          var cont = true
-          while (cont) {
+          while ({
             m = file.read(buf)
             if (m != -1) i += m
-            cont = (m != -1 && n > i)
-          }
+            m != -1 && n > i
+          }) ()
 
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
diff -r 0caf8528b07b -r a068fb7346ef 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