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