more robust interrupt handling, notably for Build_Job.terminate();
authorwenzelm
Mon, 27 Feb 2023 15:25:46 +0100
changeset 77399 375c6b9ce9ea
parent 77398 19e9cafaafc5
child 77400 f3e5b3fe230e
more robust interrupt handling, notably for Build_Job.terminate();
src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Feb 27 15:09:59 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Feb 27 15:25:46 2023 +0100
@@ -62,6 +62,8 @@
 
     private lazy val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
+        Exn.Interrupt.expose()
+
         val parent = info.parent.getOrElse("")
 
         val env =
@@ -269,10 +271,12 @@
         val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
         val process =
-          Isabelle_Process.start(store, options, session, session_background,
-            logic = parent, raw_ml_system = is_pure,
-            use_prelude = use_prelude, eval_main = eval_main,
-            cwd = info.dir.file, env = env)
+          Isabelle_Thread.uninterruptible {
+            Isabelle_Process.start(store, options, session, session_background,
+              logic = parent, raw_ml_system = is_pure,
+              use_prelude = use_prelude, eval_main = eval_main,
+              cwd = info.dir.file, env = env)
+          }
 
         val build_errors =
           Isabelle_Thread.interrupt_handler(_ => process.terminate()) {