# HG changeset patch
# User wenzelm
# Date 1586289123 -7200
# Node ID 0cb14b7455ee4c15d75ea931e808191241d33617
# Parent  a5fda30edae2b7d9e91d18ac4e0200e96b0c4d33
more careful handling of interrupts, notably for Isabelle/jEdit Scala Console;

diff -r a5fda30edae2 -r 0cb14b7455ee 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(