# HG changeset patch
# User wenzelm
# Date 1621164867 -7200
# Node ID 7202e12cb3241b387eaa3ef55033cdd45cfb9a6d
# Parent  d83e7e444b4382a65834b397bd5c7fefee9d56fe
tuned signature --- following hints by IntelliJ IDEA;

diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun May 16 13:34:27 2021 +0200
@@ -541,7 +541,7 @@
         {
           running.partition(_.is_finished) match {
             case (Nil, Nil) =>
-            case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running)
+            case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running)
             case (_ :: _, remaining) => join(remaining)
           }
         }
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 16 13:34:27 2021 +0200
@@ -376,7 +376,7 @@
 
           while (repos.importing) {
             progress.echo("Awaiting remote repository ...")
-            Time.seconds(0.5).sleep
+            Time.seconds(0.5).sleep()
             repos = phabricator.the_repository(repos.phid)
           }
 
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/General/ssh.scala	Sun May 16 13:34:27 2021 +0200
@@ -243,7 +243,7 @@
 
     val exit_status: Future[Int] =
       Future.thread("ssh_wait") {
-        while (!channel.isClosed) exec_wait_delay.sleep
+        while (!channel.isClosed) exec_wait_delay.sleep()
         channel.getExitStatus
       }
 
@@ -282,7 +282,7 @@
             if (line_buffer.size > 0) line_flush()
             finished = true
           }
-          else exec_wait_delay.sleep
+          else exec_wait_delay.sleep()
         }
 
         result.toList
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/General/time.scala	Sun May 16 13:34:27 2021 +0200
@@ -65,5 +65,5 @@
 
   def instant: Instant = Instant.ofEpochMilli(ms)
 
-  def sleep: Unit = Thread.sleep(ms)
+  def sleep(): Unit = Thread.sleep(ms)
 }
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/PIDE/prover.scala	Sun May 16 13:34:27 2021 +0200
@@ -140,7 +140,7 @@
           }
           catch { case _: IOException => finished = Some(false) }
         }
-        Time.seconds(0.05).sleep
+        Time.seconds(0.05).sleep()
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
@@ -181,7 +181,7 @@
 
     var count = 10
     while (!process_result.is_finished && count > 0) {
-      Time.seconds(0.1).sleep
+      Time.seconds(0.1).sleep()
       count -= 1
     }
     if (!process_result.is_finished) terminate_process()
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/PIDE/session.scala	Sun May 16 13:34:27 2021 +0200
@@ -719,7 +719,7 @@
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
-      output_delay.sleep
+      output_delay.sleep()
       await_stable_snapshot()
     }
     else snapshot
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/System/bash.scala	Sun May 16 13:34:27 2021 +0200
@@ -122,7 +122,7 @@
         Isabelle_System.process_signal(group_pid, signal = s)
         val running = root_process_alive() || Isabelle_System.process_signal(group_pid)
         if (running) {
-          Time.seconds(0.1).sleep
+          Time.seconds(0.1).sleep()
           signal(s, count - 1)
         }
         else false
@@ -210,7 +210,7 @@
         yield {
           Future.thread("bash_watchdog") {
             while (proc.isAlive) {
-              time.sleep
+              time.sleep()
               if (check(this)) interrupt()
             }
           }
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/System/scala.scala	Sun May 16 13:34:27 2021 +0200
@@ -69,7 +69,7 @@
           case _ => error("Malformed argument: " + quote(seconds))
         }
       val t0 = Time.now()
-      t.sleep
+      t.sleep()
       val t1 = Time.now()
       (t1 - t0).toString
     }
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 16 13:34:27 2021 +0200
@@ -290,7 +290,7 @@
     }
 
     def sleep(): Unit =
-      Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep }
+      Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
diff -r d83e7e444b43 -r 7202e12cb324 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Pure/Tools/server.scala	Sun May 16 13:34:27 2021 +0200
@@ -445,7 +445,7 @@
         find(db, name) match {
           case Some(server_info) =>
             using(server_info.connection())(_.write_message("shutdown"))
-            while(server_info.active) { Time.seconds(0.05).sleep }
+            while(server_info.active) { Time.seconds(0.05).sleep() }
             true
           case None => false
         }
diff -r d83e7e444b43 -r 7202e12cb324 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun May 16 13:34:27 2021 +0200
@@ -370,7 +370,7 @@
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
-      PIDE.options.seconds("editor_output_delay").sleep
+      PIDE.options.seconds("editor_output_delay").sleep()
       await_stable_snapshot()
     }
     else snapshot
diff -r d83e7e444b43 -r 7202e12cb324 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Sun May 16 13:14:16 2021 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Sun May 16 13:34:27 2021 +0200
@@ -36,7 +36,7 @@
         if (global_out == null) System.out.print(str)
         else global_out.writeAttrs(null, str)
       }
-      Time.seconds(0.01).sleep  // FIXME adhoc delay to avoid loosing output
+      Time.seconds(0.01).sleep()  // FIXME adhoc delay to avoid loosing output
     }
 
     override def close(): Unit = flush()