--- a/src/Pure/ML/ml_console.scala Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/ML/ml_console.scala Sat Aug 07 21:25:47 2021 +0200
@@ -75,8 +75,8 @@
options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
POSIX_Interrupt.handler { process.interrupt() } {
- new TTY_Loop(process.stdin, process.stdout).join
- val rc = process.join
+ new TTY_Loop(process.stdin, process.stdout).join()
+ val rc = process.join()
if (rc != 0) sys.exit(rc)
}
}
--- a/src/Pure/PIDE/prover.scala Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/PIDE/prover.scala Sat Aug 07 21:25:47 2021 +0200
@@ -110,7 +110,7 @@
private val process_result: Future[Process_Result] =
Future.thread("process_result") {
- val rc = process.join
+ val rc = process.join()
val timing = process.get_timing
Process_Result(rc, timing = timing)
}
--- a/src/Pure/System/bash.scala Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/System/bash.scala Sat Aug 07 21:25:47 2021 +0200
@@ -183,9 +183,9 @@
// join
- def join: Int =
+ def join(): Int =
{
- val rc = proc.waitFor
+ val rc = proc.waitFor()
do_cleanup()
rc
}
@@ -218,7 +218,7 @@
}
val rc =
- try { join }
+ try { join() }
catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
watchdog_thread.foreach(_.cancel())
--- a/src/Pure/System/tty_loop.scala Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/System/tty_loop.scala Sat Aug 07 21:25:47 2021 +0200
@@ -62,7 +62,7 @@
catch { case e: IOException => case Exn.Interrupt() => }
}
- def join: Unit = { console_output.join; console_input.join }
+ def join(): Unit = { console_output.join; console_input.join }
def cancel(): Unit = console_input.cancel()
}
--- a/src/Pure/Tools/server.scala Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/Tools/server.scala Sat Aug 07 21:25:47 2021 +0200
@@ -508,7 +508,7 @@
init(name, port = port, existing_server = existing_server, log = log)
Output.writeln(server_info.toString, stdout = true)
if (console) {
- using(server_info.connection())(connection => connection.tty_loop().join)
+ using(server_info.connection())(connection => connection.tty_loop().join())
}
server.foreach(_.join())
}