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