# HG changeset patch
# User wenzelm
# Date 1559418183 -7200
# Node ID 9f2a6856b912207e7ecb67580c4632f3e3a58206
# Parent  22c7eee0dd564d55e646dee32bb8901ead58f92d
tuned -- accommodate scala-2.13.0-RC3;

diff -r 22c7eee0dd56 -r 9f2a6856b912 src/Pure/PIDE/prover.scala
--- 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
diff -r 22c7eee0dd56 -r 9f2a6856b912 src/Pure/System/tty_loop.scala
--- 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()