# HG changeset patch
# User wenzelm
# Date 1648759234 -7200
# Node ID 81673c441ce390f806526267751cfb8a2aefc649
# Parent  8b7497992301f6d267d7a37e17eb567e10bc2bec
tuned: eliminted do-while for the sake of scala3;

diff -r 8b7497992301 -r 81673c441ce3 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Thu Mar 31 22:24:11 2022 +0200
+++ b/src/Pure/General/bytes.scala	Thu Mar 31 22:40:34 2022 +0200
@@ -75,10 +75,12 @@
       val buf = new Array[Byte](8192)
       var m = 0
 
-      do {
+      var cont = true
+      while (cont) {
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
-      } while (m != -1 && limit > out.size)
+        cont = (m != -1 && limit > out.size)
+      }
 
       new Bytes(out.toByteArray, 0, out.size)
     }
diff -r 8b7497992301 -r 81673c441ce3 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Thu Mar 31 22:24:11 2022 +0200
+++ b/src/Pure/General/sha1.scala	Thu Mar 31 22:40:34 2022 +0200
@@ -40,10 +40,12 @@
       {
         val buf = new Array[Byte](65536)
         var m = 0
-        do {
+        var cont = true
+        while (cont) {
           m = stream.read(buf, 0, buf.length)
           if (m != -1) sha.update(buf, 0, m)
-        } while (m != -1)
+          cont = (m != -1)
+        }
       }))
 
   def digest(path: Path): Digest = digest(path.file)
diff -r 8b7497992301 -r 81673c441ce3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 31 22:24:11 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 31 22:40:34 2022 +0200
@@ -1150,11 +1150,12 @@
           val buf = ByteBuffer.allocate(n)
           var i = 0
           var m = 0
-          do {
+          var cont = true
+          while (cont) {
             m = file.read(buf)
             if (m != -1) i += m
+            cont = (m != -1 && n > i)
           }
-          while (m != -1 && n > i)
 
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
diff -r 8b7497992301 -r 81673c441ce3 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Thu Mar 31 22:24:11 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala	Thu Mar 31 22:40:34 2022 +0200
@@ -951,12 +951,14 @@
       val results = new mutable.ListBuffer[A]
       var after = ""
 
-      do {
+      var cont = true
+      while (cont) {
         val result =
           execute(method, params = params ++ JSON.optional("after" -> proper_string(after)))
         results ++= result.get_value(JSON.list(_, "data", unapply))
         after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after")))
-      } while (after.nonEmpty)
+        cont = after.nonEmpty
+      }
 
       results.toList
     }
diff -r 8b7497992301 -r 81673c441ce3 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Mar 31 22:24:11 2022 +0200
+++ b/src/Pure/library.scala	Thu Mar 31 22:40:34 2022 +0200
@@ -75,7 +75,12 @@
       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