--- 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)
}
--- 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)
--- 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)
--- 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
}
--- 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