--- a/src/Pure/System/tty_loop.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/System/tty_loop.scala Wed Jan 15 19:54:50 2020 +0100
@@ -21,12 +21,12 @@
while (!finished) {
var c = -1
var done = false
- while (!done && (result.length == 0 || reader.ready)) {
+ while (!done && (result.isEmpty || reader.ready)) {
c = reader.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
- if (result.length > 0) {
+ if (result.nonEmpty) {
System.out.print(result.toString)
System.out.flush()
result.clear