--- a/src/Pure/Concurrent/task_queue.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Thu Sep 21 23:45:03 2023 +0200
@@ -296,7 +296,7 @@
fun cancel (Queue {groups, jobs, ...}) group =
let
- val _ = cancel_group group Exn.Interrupt;
+ val _ = cancel_group group Isabelle_Thread.interrupt;
val running =
Tasks.fold (fn task =>
(case get_job jobs task of Running thread => insert Isabelle_Thread.equal thread | _ => I))
@@ -308,7 +308,7 @@
fun cancel_job (task, (job, _)) (groups, running) =
let
val group = group_of_task task;
- val _ = cancel_group group Exn.Interrupt;
+ val _ = cancel_group group Isabelle_Thread.interrupt;
in
(case job of
Running t => (insert eq_group group groups, insert Isabelle_Thread.equal t running)