tuned signature;
authorwenzelm
Sat, 07 Aug 2021 21:25:47 +0200
changeset 74141 bba35ad317ab
parent 74140 8a5e02ef975c
child 74142 0f051404f487
tuned signature;
src/Pure/ML/ml_console.scala
src/Pure/PIDE/prover.scala
src/Pure/System/bash.scala
src/Pure/System/tty_loop.scala
src/Pure/Tools/server.scala
--- 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())
       }