--- a/src/Pure/PIDE/prover.scala Sat Jun 01 13:53:23 2019 +0200
+++ b/src/Pure/PIDE/prover.scala Sat Jun 01 21:43:03 2019 +0200
@@ -231,7 +231,7 @@
}
if (result.length > 0) {
output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
- result.length = 0
+ result.clear
}
else {
reader.close
--- a/src/Pure/System/tty_loop.scala Sat Jun 01 13:53:23 2019 +0200
+++ b/src/Pure/System/tty_loop.scala Sat Jun 01 21:43:03 2019 +0200
@@ -29,7 +29,7 @@
if (result.length > 0) {
System.out.print(result.toString)
System.out.flush()
- result.length = 0
+ result.clear
}
else {
reader.close()