--- a/src/Doc/Implementation/ML.thy Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Doc/Implementation/ML.thy Thu Sep 21 23:45:03 2023 +0200
@@ -1121,7 +1121,8 @@
text \<open>
These indicate arbitrary system events: both the ML runtime system and the
Isabelle/ML infrastructure signal various exceptional situations by raising
- the special \<^ML>\<open>Exn.Interrupt\<close> exception in user code.
+ special exceptions user code, satisfying the predicate
+ \<^ML>\<open>Exn.is_interrupt\<close>.
This is the one and only way that physical events can intrude an Isabelle/ML
program. Such an interrupt can mean out-of-memory, stack overflow, timeout,
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Sep 21 23:45:03 2023 +0200
@@ -1049,7 +1049,7 @@
in
if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
else if rc = 2 then TimedOut js
- else if rc = 130 then Exn.interrupt ()
+ else if rc = 130 then Isabelle_Thread.interrupt_self ()
else Error (if first_error = "" then "Unknown error" else first_error, js)
end
end
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Sep 21 23:45:03 2023 +0200
@@ -102,7 +102,7 @@
NONE
else
let
- val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling
+ val _ = List.app (Isabelle_Thread.interrupt_other o #1) canceling
val canceling' = filter (Isabelle_Thread.is_active o #1) canceling
val state' = make_state manager timeout_heap' active canceling' messages
in SOME (map #2 timeout_threads, state') end
--- a/src/Pure/Concurrent/future.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Sep 21 23:45:03 2023 +0200
@@ -195,13 +195,13 @@
val running = Task_Queue.cancel (! queue) group;
val _ = running |> List.app (fn thread =>
if Isabelle_Thread.is_self thread then ()
- else Isabelle_Thread.interrupt_unsynchronized thread);
+ else Isabelle_Thread.interrupt_other thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)
let
val (groups, threads) = Task_Queue.cancel_all (! queue);
- val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads;
+ val _ = List.app Isabelle_Thread.interrupt_other threads;
in groups end;
fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -450,7 +450,7 @@
Exn.capture (fn () =>
Thread_Attributes.with_attributes atts (fn _ =>
(Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
- else Exn.interrupt_exn;
+ else Isabelle_Thread.interrupt_exn;
in assign_result group result (identify_result pos res) end;
in (result, job) end;
@@ -645,7 +645,7 @@
let
val group = worker_subgroup ();
val result = Single_Assignment.var "promise" : 'a result;
- fun assign () = assign_result group result Exn.interrupt_exn
+ fun assign () = assign_result group result Isabelle_Thread.interrupt_exn
handle Fail _ => true
| exn =>
if Exn.is_interrupt exn
@@ -665,7 +665,8 @@
val group = Task_Queue.group_of_task task;
val pos = Position.thread_data ();
fun job ok =
- assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
+ assign_result group result
+ (if ok then identify_result pos res else Isabelle_Thread.interrupt_exn);
val _ =
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
let
--- a/src/Pure/Concurrent/isabelle_thread.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Thu Sep 21 23:45:03 2023 +0200
@@ -20,7 +20,10 @@
val fork: params -> (unit -> unit) -> T
val is_active: T -> bool
val join: T -> unit
- val interrupt_unsynchronized: T -> unit
+ val interrupt: exn
+ val interrupt_exn: 'a Exn.result
+ val interrupt_self: unit -> 'a
+ val interrupt_other: T -> unit
end;
structure Isabelle_Thread: ISABELLE_THREAD =
@@ -102,9 +105,14 @@
do OS.Process.sleep (seconds 0.1);
-(* interrupt *)
+(* interrupts *)
-fun interrupt_unsynchronized t =
+val interrupt = Thread.Thread.Interrupt;
+val interrupt_exn = Exn.Exn interrupt;
+
+fun interrupt_self () = raise interrupt;
+
+fun interrupt_other t =
Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
end;
--- a/src/Pure/Concurrent/par_exn.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/Concurrent/par_exn.ML Thu Sep 21 23:45:03 2023 +0200
@@ -21,7 +21,7 @@
exception Par_Exn of exn list;
(*non-empty list with unique identified elements sorted by Exn_Properties.ord;
- no occurrences of Par_Exn or Exn.Interrupt*)
+ no occurrences of Par_Exn or Exn.is_interrupt*)
fun par_exns (Par_Exn exns) = exns
| par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn];
@@ -30,7 +30,7 @@
let
val exnss = map par_exns exns;
val exns' = Ord_List.unions Exn_Properties.ord exnss handle Option.Option => flat exnss;
- in if null exns' then Exn.Interrupt else Par_Exn exns' end;
+ in if null exns' then Isabelle_Thread.interrupt else Par_Exn exns' end;
fun dest (Par_Exn exns) = SOME exns
| dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
--- 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)
--- a/src/Pure/Concurrent/timeout.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML Thu Sep 21 23:45:03 2023 +0200
@@ -40,7 +40,7 @@
val request =
Event_Timer.request {physical = physical} (start + scale_time timeout)
- (fn () => Isabelle_Thread.interrupt_unsynchronized self);
+ (fn () => Isabelle_Thread.interrupt_other self);
val result =
Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
--- a/src/Pure/General/exn.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/General/exn.ML Thu Sep 21 23:45:03 2023 +0200
@@ -26,10 +26,7 @@
val map_res: ('a -> 'b) -> 'a result -> 'b result
val maps_res: ('a -> 'b result) -> 'a result -> 'b result
val map_exn: (exn -> exn) -> 'a result -> 'a result
- exception Interrupt
- val interrupt: unit -> 'a
val is_interrupt: exn -> bool
- val interrupt_exn: 'a result
val is_interrupt_exn: 'a result -> bool
val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
val failure_rc: exn -> int
@@ -92,16 +89,10 @@
(* interrupts *)
-exception Interrupt = Thread.Thread.Interrupt;
-
-fun interrupt () = raise Interrupt;
-
-fun is_interrupt Interrupt = true
+fun is_interrupt Thread.Thread.Interrupt = true
| is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
| is_interrupt _ = false;
-val interrupt_exn = Exn Interrupt;
-
fun is_interrupt_exn (Exn exn) = is_interrupt exn
| is_interrupt_exn _ = false;
--- a/src/Pure/PIDE/command.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/PIDE/command.ML Thu Sep 21 23:45:03 2023 +0200
@@ -241,7 +241,9 @@
let
val _ = status tr Markup.failed;
val _ = status tr Markup.finished;
- val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else ();
+ val _ =
+ if null errs then (status tr Markup.canceled; Isabelle_Thread.interrupt_self ())
+ else ();
in {failed = true, command = tr, state = st} end
| SOME st' =>
let
--- a/src/Pure/System/isabelle_system.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML Thu Sep 21 23:45:03 2023 +0200
@@ -68,7 +68,7 @@
if head = Bash.server_uuid andalso length args = 1 then
loop (SOME (hd args)) s
else if head = Bash.server_interrupt andalso null args then
- Exn.interrupt ()
+ Isabelle_Thread.interrupt_self ()
else if head = Bash.server_failure andalso length args = 1 then
raise Fail (hd args)
else if head = Bash.server_result andalso length args >= 4 then
--- a/src/Pure/System/scala.ML Thu Sep 21 18:17:26 2023 +0200
+++ b/src/Pure/System/scala.ML Thu Sep 21 23:45:03 2023 +0200
@@ -35,7 +35,7 @@
| ("1", _) => Exn.Res rest
| ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg))
| ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg))
- | ("4", []) => Exn.interrupt_exn
+ | ("4", []) => Isabelle_Thread.interrupt_exn
| _ => raise Fail "Malformed Scala.result");
in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end);
@@ -57,7 +57,7 @@
(case Symtab.lookup tab id of
SOME (Exn.Exn Match) => NONE
| SOME result => SOME (result, Symtab.delete id tab)
- | NONE => SOME (Exn.interrupt_exn, tab)));
+ | NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
in
invoke ();
Exn.release (restore_attributes await_result ())