diff -r 19e9cafaafc5 -r 375c6b9ce9ea 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()) {