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