revert pointless 375c6b9ce9ea: overall thread context is already uninterruptible (see 54ac957c53ec);
--- a/src/Pure/Tools/build_job.scala Tue Feb 28 14:13:50 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Feb 28 14:20:57 2023 +0100
@@ -62,8 +62,6 @@
private lazy val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
- Exn.Interrupt.expose()
-
val parent = info.parent.getOrElse("")
val env =
@@ -271,12 +269,10 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
- 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)
- }
+ 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()) {