more careful handling of interrupts, notably for Isabelle/jEdit Scala Console;
authorwenzelm
Tue, 07 Apr 2020 21:52:03 +0200
changeset 71943 0cb14b7455ee
parent 71942 a5fda30edae2
child 71944 c986a422dee1
child 71947 d8e60a0ffa02
more careful handling of interrupts, notably for Isabelle/jEdit Scala Console;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 07 21:49:36 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 07 21:52:03 2020 +0200
@@ -594,8 +594,7 @@
 
     def sleep()
     {
-      try { Time.seconds(0.5).sleep }
-      catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
+      Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
     }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
@@ -750,7 +749,7 @@
         progress.echo_warning("Nothing to build")
         Map.empty[String, Result]
       }
-      else loop(queue, Map.empty, Map.empty)
+      else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
     val results =
       new Results(