# HG changeset patch # User wenzelm # Date 1586016785 -7200 # Node ID 5036edb025b75640938a262753e14dba17733821 # Parent fd487d261169624e8d47d46c247b7cc45bc5cb2a clarified signature; diff -r fd487d261169 -r 5036edb025b7 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Apr 04 18:13:05 2020 +0200 @@ -514,7 +514,7 @@ { running.partition(_.is_finished) match { case (Nil, Nil) => - case (Nil, _ :: _) => Thread.sleep(500); join(running) + case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running) case (_ :: _, remaining) => join(remaining) } } diff -r fd487d261169 -r 5036edb025b7 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/General/mercurial.scala Sat Apr 04 18:13:05 2020 +0200 @@ -274,7 +274,7 @@ while (repos.importing) { progress.echo("Awaiting remote repository ...") - Thread.sleep(500) + Time.seconds(0.5).sleep repos = phabricator.the_repository(repos.phid) } diff -r fd487d261169 -r 5036edb025b7 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/General/ssh.scala Sat Apr 04 18:13:05 2020 +0200 @@ -237,7 +237,7 @@ val exit_status: Future[Int] = Future.thread("ssh_wait") { - while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms) + while (!channel.isClosed) exec_wait_delay.sleep channel.getExitStatus } @@ -276,7 +276,7 @@ if (line_buffer.size > 0) line_flush() finished = true } - else Thread.sleep(exec_wait_delay.ms) + else exec_wait_delay.sleep } result.toList diff -r fd487d261169 -r 5036edb025b7 src/Pure/General/time.scala --- a/src/Pure/General/time.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/General/time.scala Sat Apr 04 18:13:05 2020 +0200 @@ -65,4 +65,6 @@ } def instant: Instant = Instant.ofEpochMilli(ms) + + def sleep { Thread.sleep(ms) } } diff -r fd487d261169 -r 5036edb025b7 src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/PIDE/prover.scala Sat Apr 04 18:13:05 2020 +0200 @@ -129,7 +129,7 @@ } catch { case _: IOException => finished = Some(false) } } - Thread.sleep(50) + Time.seconds(0.05).sleep } (finished.isEmpty || !finished.get, result.toString.trim) } @@ -170,7 +170,7 @@ var count = 10 while (!process_result.is_finished && count > 0) { - Thread.sleep(100) + Time.seconds(0.1).sleep count -= 1 } if (!process_result.is_finished) terminate_process() diff -r fd487d261169 -r 5036edb025b7 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/PIDE/session.scala Sat Apr 04 18:13:05 2020 +0200 @@ -687,7 +687,7 @@ { val snapshot = this.snapshot() if (snapshot.is_outdated) { - Thread.sleep(output_delay.ms) + output_delay.sleep await_stable_snapshot() } else snapshot diff -r fd487d261169 -r 5036edb025b7 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/System/bash.scala Sat Apr 04 18:13:05 2020 +0200 @@ -115,7 +115,7 @@ while (running && count > 0) { if (kill(signal)) { Exn.Interrupt.postpone { - Thread.sleep(100) + Time.seconds(0.1).sleep count -= 1 } } diff -r fd487d261169 -r 5036edb025b7 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/Tools/build.scala Sat Apr 04 18:13:05 2020 +0200 @@ -584,7 +584,7 @@ def sleep() { - try { Thread.sleep(500) } + try { Time.seconds(0.5).sleep } catch { case Exn.Interrupt() => Exn.Interrupt.impose() } } diff -r fd487d261169 -r 5036edb025b7 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/Tools/server.scala Sat Apr 04 18:13:05 2020 +0200 @@ -442,7 +442,7 @@ find(db, name) match { case Some(server_info) => using(server_info.connection())(_.write_message("shutdown")) - while(server_info.active) { Thread.sleep(50) } + while(server_info.active) { Time.seconds(0.05).sleep } true case None => false } diff -r fd487d261169 -r 5036edb025b7 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Apr 04 18:13:05 2020 +0200 @@ -365,7 +365,7 @@ { val snapshot = this.snapshot() if (snapshot.is_outdated) { - Thread.sleep(PIDE.options.seconds("editor_output_delay").ms) + PIDE.options.seconds("editor_output_delay").sleep await_stable_snapshot() } else snapshot diff -r fd487d261169 -r 5036edb025b7 src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Tools/jEdit/src/scala_console.scala Sat Apr 04 18:13:05 2020 +0200 @@ -64,7 +64,7 @@ if (global_out == null) System.out.print(str) else global_out.writeAttrs(null, str) } - Thread.sleep(10) // FIXME adhoc delay to avoid loosing output + Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output } override def close() { flush () }