--- a/src/Tools/jEdit/src/scala_console.scala Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Thu Mar 04 21:04:27 2021 +0100
@@ -30,7 +30,7 @@
override def flush(): Unit =
{
- val s = buf.synchronized { val s = buf.toString; buf.clear; s }
+ val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
val str = UTF8.decode_permissive(s)
GUI_Thread.later {
if (global_out == null) System.out.print(str)
@@ -97,7 +97,7 @@
private class Interpreter
{
private val running = Synchronized[Option[Thread]](None)
- def interrupt: Unit = running.change(opt => { opt.foreach(_.interrupt); opt })
+ def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
private val interp =
Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
@@ -146,8 +146,8 @@
{
interpreters.get(console) match {
case Some(interp) =>
- interp.interrupt
- interp.thread.shutdown
+ interp.interrupt()
+ interp.thread.shutdown()
interpreters -= console
case None =>
}
@@ -177,5 +177,5 @@
}
override def stop(console: Console): Unit =
- interpreters.get(console).foreach(_.interrupt)
+ interpreters.get(console).foreach(_.interrupt())
}