# HG changeset patch
# User wenzelm
# Date 1628359118 -7200
# Node ID 8a5e02ef975c443b94788ff1b254ae73a647d13c
# Parent  3314559ef095c0698028bb2fbe2f4fd8eac7f63c
clarified signature;

diff -r 3314559ef095 -r 8a5e02ef975c src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Sat Aug 07 19:29:41 2021 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Sat Aug 07 19:58:38 2021 +0200
@@ -119,6 +119,6 @@
   def shutdown(): Unit =
   {
     synchronized { if (is_active) { active = false; mailbox.send(None) } }
-    thread.join
+    thread.join()
   }
 }
diff -r 3314559ef095 -r 8a5e02ef975c src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Sat Aug 07 19:29:41 2021 +0200
+++ b/src/Pure/General/file_watcher.scala	Sat Aug 07 19:58:38 2021 +0200
@@ -129,7 +129,7 @@
     override def shutdown(): Unit =
     {
       watcher_thread.interrupt()
-      watcher_thread.join
+      watcher_thread.join()
       delay_changed.revoke()
     }
   }
diff -r 3314559ef095 -r 8a5e02ef975c src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Aug 07 19:29:41 2021 +0200
+++ b/src/Pure/PIDE/prover.scala	Sat Aug 07 19:58:38 2021 +0200
@@ -162,7 +162,7 @@
       val result = process_result.join
       system_output("process terminated")
       command_input_close()
-      for (thread <- List(stdout, stderr, message)) thread.join
+      for (thread <- List(stdout, stderr, message)) thread.join()
       system_output("process_manager terminated")
       exit_message(result)
     }
diff -r 3314559ef095 -r 8a5e02ef975c src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Sat Aug 07 19:29:41 2021 +0200
+++ b/src/Pure/System/command_line.scala	Sat Aug 07 19:58:38 2021 +0200
@@ -34,7 +34,7 @@
           }
         sys.exit(rc)
       }
-    thread.join
+    thread.join()
   }
 
   def ML_tool(body: List[String]): String =
diff -r 3314559ef095 -r 8a5e02ef975c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Aug 07 19:29:41 2021 +0200
+++ b/src/Pure/Tools/server.scala	Sat Aug 07 19:58:38 2021 +0200
@@ -150,8 +150,8 @@
       }
 
     def start(): Unit = thread
-    def join: Unit = thread.join
-    def stop(): Unit = { socket.close(); join }
+    def join(): Unit = thread.join()
+    def stop(): Unit = { socket.close(); join() }
   }
 
 
@@ -255,7 +255,7 @@
     def close(): Unit =
     {
       while(_tasks.change_result(tasks => { tasks.foreach(_.cancel()); (tasks.nonEmpty, tasks) }))
-      { _tasks.value.foreach(_.join) }
+      { _tasks.value.foreach(_.join()) }
     }
   }
 
@@ -307,8 +307,8 @@
       progress.stop()
       context.remove_task(task)
     }
-    def start: Unit = thread
-    def join: Unit = thread.join
+    def start(): Unit = thread
+    def join(): Unit = thread.join()
   }
 
 
@@ -510,7 +510,7 @@
         if (console) {
           using(server_info.connection())(connection => connection.tty_loop().join)
         }
-        server.foreach(_.join)
+        server.foreach(_.join())
       }
     })
 }
@@ -546,7 +546,7 @@
     }
   }
 
-  override def join: Unit = { super.join; shutdown() }
+  override def join(): Unit = { super.join(); shutdown() }
 
   override def handle(connection: Server.Connection): Unit =
   {
@@ -572,7 +572,7 @@
                       Exn.capture { cmd.command_body((context, arg)) } match {
                         case Exn.Res(task: Server.Task) =>
                           connection.reply_ok(JSON.Object(task.ident))
-                          task.start
+                          task.start()
                         case Exn.Res(res) => connection.reply_ok(res)
                         case Exn.Exn(exn) =>
                           val err = Server.json_error(exn)