--- 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)
}
}
--- 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)
}
--- 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
--- 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)
}
--- 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()
--- 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
--- 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()
}
}
--- 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
}
--- 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)
--- 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
}
--- 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
--- 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()