--- a/NEWS Thu Oct 12 12:36:09 2023 +0100
+++ b/NEWS Thu Oct 12 21:13:22 2023 +0200
@@ -33,6 +33,12 @@
INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
as last resort declare [[ML_catch_all]] within the theory context.
+* Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML
+runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error.
+Exn.is_interrupt covers all kinds of interrupts as before, but
+Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more
+specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
+
*** HOL ***
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Oct 12 21:13:22 2023 +0200
@@ -18,9 +18,6 @@
structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY =
struct
-fun make_thread interrupts body =
- Isabelle_Thread.fork {name = "async_manager", stack_limit = NONE, interrupts = interrupts} body;
-
fun implode_message (workers, work) =
space_implode " " (Try.serial_commas "and" workers) ^ work
@@ -86,7 +83,7 @@
fun check_thread_manager () = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages} =>
if (case manager of SOME thread => Isabelle_Thread.is_active thread | NONE => false) then state
- else let val manager = SOME (make_thread false (fn () =>
+ else let val manager = SOME (Isabelle_Thread.fork (Isabelle_Thread.params "async_manager") (fn () =>
let
fun time_limit timeout_heap =
(case try Thread_Heap.min timeout_heap of
@@ -135,7 +132,7 @@
check_thread_manager ())
fun thread tool birth_time death_time desc f =
- (make_thread true
+ (Isabelle_Thread.fork (Isabelle_Thread.params "async_worker" |> Isabelle_Thread.interrupts)
(fn () =>
let
val self = Isabelle_Thread.self ()
--- a/src/Pure/Admin/build_log.scala Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Thu Oct 12 21:13:22 2023 +0200
@@ -820,7 +820,7 @@
class Store private[Build_Log](val options: Options, val cache: XML.Cache) {
override def toString: String = {
val s =
- Exn.capture { open_database() } match {
+ Exn.result { open_database() } match {
case Exn.Res(db) =>
val db_name = db.toString
db.close()
@@ -1036,7 +1036,7 @@
for (file_group <- file_groups) {
val log_files =
Par_List.map[JFile, Exn.Result[Log_File]](
- file => Exn.capture { Log_File(file) }, file_group)
+ file => Exn.result { Log_File(file) }, file_group)
db.transaction {
for (case Exn.Res(log_file) <- log_files) {
progress.echo("Log " + quote(log_file.name), verbose = true)
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Oct 12 21:13:22 2023 +0200
@@ -481,7 +481,7 @@
def run_task(start_date: Date, task: Logger_Task): Unit = {
val logger = start_logger(start_date, task.name)
- val res = Exn.capture { task.body(logger) }
+ val res = Exn.result { task.body(logger) }
val end_date = Date.now()
val err =
res match {
--- a/src/Pure/Concurrent/event_timer.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/event_timer.ML Thu Oct 12 21:13:22 2023 +0200
@@ -118,7 +118,7 @@
(case next_event (Time.now (), ML_Heap.gc_now ()) requests of
SOME (event, requests') =>
let
- val _ = Exn.capture event ();
+ val _ = Exn.capture_body event; (*sic!*)
val state' = make_state (requests', status, manager);
in SOME (true, state') end
| NONE =>
@@ -129,9 +129,7 @@
fun manager_check manager =
if is_some manager andalso Isabelle_Thread.is_active (the manager) then manager
- else
- SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
- manager_loop);
+ else SOME (Isabelle_Thread.fork (Isabelle_Thread.params "event_timer") manager_loop);
fun shutdown () =
Thread_Attributes.uninterruptible_body (fn run =>
@@ -141,14 +139,17 @@
raise Fail "Concurrent attempt to shutdown event timer"
else (true, make_state (requests, Shutdown_Req, manager_check manager)))
then
- run (fn () =>
- Synchronized.guarded_access state
- (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) ()
- handle exn =>
- if Exn.is_interrupt exn then
+ let
+ fun main () =
+ Synchronized.guarded_access state
+ (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE);
+ val result = Exn.capture_body (run main);
+ in
+ if Exn.is_interrupt_exn result then
Synchronized.change state (fn State {requests, manager, ...} =>
make_state (requests, Normal, manager))
- else ()
+ else Exn.release result
+ end
else ());
--- a/src/Pure/Concurrent/future.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Oct 12 21:13:22 2023 +0200
@@ -236,7 +236,7 @@
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
val test = Isabelle_Thread.expose_interrupt_result ();
val _ =
- if ok andalso not (Exn.is_interrupt_exn test) then ()
+ if ok andalso not (Exn.is_interrupt_proper_exn test) then ()
else if null (cancel_now group) then ()
else cancel_later group;
val _ = broadcast work_finished;
@@ -269,10 +269,7 @@
fun worker_start name = (*requires SYNCHRONIZED*)
let
- val worker =
- Isabelle_Thread.fork
- {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
- (fn () => worker_loop name);
+ val worker = Isabelle_Thread.fork (Isabelle_Thread.params "worker") (fn () => worker_loop name);
in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -282,7 +279,7 @@
fun scheduler_end () = (*requires SYNCHRONIZED*)
(ML_statistics (); scheduler := NONE);
-fun scheduler_next () = (*requires SYNCHRONIZED*)
+fun scheduler_next0 () = (*requires SYNCHRONIZED*)
let
val now = Time.now ();
val tick = ! last_round + next_round <= now;
@@ -357,15 +354,19 @@
val _ = if continue then () else scheduler_end ();
val _ = broadcast scheduler_event;
- in continue end
- handle exn =>
- (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
- if Exn.is_interrupt exn then
- (List.app cancel_later (cancel_all ());
- signal work_available; true)
- else
- (scheduler_end ();
- Exn.reraise exn));
+ in continue end;
+
+fun scheduler_next () =
+ (case Exn.capture_body scheduler_next0 of
+ Exn.Res res => res
+ | Exn.Exn exn =>
+ (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
+ if Exn.is_interrupt_proper exn then
+ (List.app cancel_later (cancel_all ());
+ signal work_available; true)
+ else
+ (scheduler_end ();
+ Exn.reraise exn)));
fun scheduler_loop () =
(while
@@ -380,10 +381,7 @@
fun scheduler_check () = (*requires SYNCHRONIZED*)
(do_shutdown := false;
if scheduler_active () then ()
- else
- scheduler :=
- SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
- scheduler_loop));
+ else scheduler := SOME (Isabelle_Thread.fork (Isabelle_Thread.params "scheduler") scheduler_loop));
@@ -423,11 +421,13 @@
fun assign_result group result res =
let
- val _ = Single_Assignment.assign result res
- handle exn as Fail _ =>
- (case Single_Assignment.peek result of
- SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
- | _ => Exn.reraise exn);
+ val _ =
+ (case Exn.capture_body (fn () => Single_Assignment.assign result res) of
+ Exn.Exn (exn as Fail _) =>
+ (case Single_Assignment.peek result of
+ SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt_proper e then e else exn)
+ | _ => Exn.reraise exn)
+ | _ => ());
val ok =
(case the (Single_Assignment.peek result) of
Exn.Exn exn =>
@@ -447,9 +447,9 @@
let
val res =
if ok then
- Exn.capture (fn () =>
+ Exn.capture_body (fn () =>
Thread_Attributes.with_attributes atts (fn _ =>
- (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
+ (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ()))
else Isabelle_Thread.interrupt_exn;
in assign_result group result (identify_result pos res) end;
in (result, job) end;
@@ -498,12 +498,12 @@
fun get_result x =
(case peek x of
NONE => Exn.Exn (Fail "Unfinished future")
- | SOME res =>
- if Exn.is_interrupt_exn res then
+ | SOME result =>
+ if Exn.is_interrupt_proper_exn result then
(case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
- [] => res
+ [] => result
| exns => Exn.Exn (Par_Exn.make exns))
- else res);
+ else result);
local
@@ -560,8 +560,11 @@
val futures =
forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
in
- run join_results futures
- handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
+ (case Exn.capture_body (fn () => run join_results futures) of
+ Exn.Res res => res
+ | Exn.Exn exn =>
+ (if Exn.is_interrupt_proper exn then cancel_group group else ();
+ Exn.reraise exn))
end);
@@ -645,12 +648,14 @@
let
val group = worker_subgroup ();
val result = Single_Assignment.var "promise" : 'a result;
- fun assign () = assign_result group result Isabelle_Thread.interrupt_exn
- handle Fail _ => true
- | exn =>
- if Exn.is_interrupt exn
- then raise Fail "Concurrent attempt to fulfill promise"
- else Exn.reraise exn;
+ fun assign () =
+ (case Exn.capture_body (fn () => assign_result group result Isabelle_Thread.interrupt_exn) of
+ Exn.Res res => res
+ | Exn.Exn (Fail _) => true
+ | Exn.Exn exn =>
+ if Exn.is_interrupt_proper exn
+ then raise Fail "Concurrent attempt to fulfill promise"
+ else Exn.reraise exn);
fun job () =
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
(fn _ => Exn.release (Exn.capture assign () before abort ()));
--- a/src/Pure/Concurrent/isabelle_thread.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.ML Thu Oct 12 21:13:22 2023 +0200
@@ -15,8 +15,11 @@
val self: unit -> T
val is_self: T -> bool
val threads_stack_limit: real Unsynchronized.ref
- val stack_limit: unit -> int option
- type params = {name: string, stack_limit: int option, interrupts: bool}
+ val default_stack_limit: unit -> int option
+ type params
+ val params: string -> params
+ val stack_limit: int -> params -> params
+ val interrupts: params -> params
val attributes: params -> Thread.Thread.threadAttribute list
val fork: params -> (unit -> unit) -> T
val is_active: T -> bool
@@ -39,7 +42,7 @@
(* abstract type *)
-abstype T = T of {thread: Thread.Thread.thread, name: string, id: int}
+abstype T = T of {thread: Thread.Thread.thread, name: string, id: int, break: bool Synchronized.var}
with
val make = T;
fun dest (T args) = args;
@@ -64,13 +67,16 @@
val self_var = Thread_Data.var () : T Thread_Data.var;
in
-fun init_self args =
- let val t = make args in Thread_Data.put self_var (SOME t); t end;
+fun init_self name =
+ let
+ val break = Synchronized.var "Isabelle_Thread.break" false;
+ val t = make {thread = Thread.Thread.self (), name = name, id = make_id (), break = break};
+ in Thread_Data.put self_var (SOME t); t end;
fun self () =
(case Thread_Data.get self_var of
SOME t => t
- | NONE => init_self {thread = Thread.Thread.self (), name = "", id = make_id ()});
+ | NONE => init_self "");
fun is_self t = equal (t, self ());
@@ -81,24 +87,39 @@
val threads_stack_limit = Unsynchronized.ref 0.25;
-fun stack_limit () =
- let
- val limit = Real.floor (! threads_stack_limit * 1024.0 * 1024.0 * 1024.0);
+fun default_stack_limit () =
+ let val limit = Real.floor (! threads_stack_limit * 1024.0 * 1024.0 * 1024.0)
in if limit <= 0 then NONE else SOME limit end;
-type params = {name: string, stack_limit: int option, interrupts: bool};
+abstype params = Params of {name: string, stack_limit: int option, interrupts: bool}
+with
+
+fun make_params (name, stack_limit, interrupts) =
+ Params {name = name, stack_limit = stack_limit, interrupts = interrupts};
+
+fun params name = make_params (name, default_stack_limit (), false);
+fun stack_limit limit (Params {name, interrupts, ...}) = make_params (name, SOME limit, interrupts);
+fun interrupts (Params {name, stack_limit, ...}) = make_params (name, stack_limit, true);
-fun attributes ({stack_limit, interrupts, ...}: params) =
- Thread.Thread.MaximumMLStack stack_limit ::
+fun params_name (Params {name, ...}) = name;
+fun params_stack_limit (Params {stack_limit, ...}) = stack_limit;
+fun params_interrupts (Params {interrupts, ...}) = interrupts;
+
+end;
+
+fun attributes params =
+ Thread.Thread.MaximumMLStack (params_stack_limit params) ::
Thread_Attributes.convert_attributes
- (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
+ (if params_interrupts params
+ then Thread_Attributes.public_interrupts
+ else Thread_Attributes.no_interrupts);
-fun fork (params: params) body =
+fun fork params body =
let
val self = Single_Assignment.var "self";
fun main () =
let
- val t = init_self {thread = Thread.Thread.self (), name = #name params, id = make_id ()};
+ val t = init_self (params_name params);
val _ = Single_Assignment.assign self t;
in body () end;
val _ = Thread.Thread.fork (main, attributes params);
@@ -116,25 +137,40 @@
(* interrupts *)
-val interrupt = Thread.Thread.Interrupt;
+val interrupt = Exn.Interrupt_Break;
val interrupt_exn = Exn.Exn interrupt;
fun interrupt_self () = raise interrupt;
fun interrupt_other t =
- Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
+ Synchronized.change (#break (dest t))
+ (fn b => (Thread.Thread.interrupt (get_thread t); true) handle Thread.Thread _ => b);
+
+fun check_interrupt exn =
+ if Exn.is_interrupt_raw exn then
+ let
+ val t = self ();
+ val break = Synchronized.change_result (#break (dest t)) (fn b => (b, false));
+ in if break then Exn.Interrupt_Break else Exn.Interrupt_Breakdown end
+ else exn;
+
+fun check_interrupt_exn result =
+ Exn.map_exn check_interrupt result;
structure Exn: EXN =
struct
open Exn;
- val capture = capture0;
+ fun capture f x = Res (f x) handle e => Exn (check_interrupt e);
+ fun capture_body e = capture e ();
end;
fun expose_interrupt_result () =
let
val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
- val _ = Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
- val test = Exn.capture Thread.Thread.testInterrupt ();
+ fun main () =
+ (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
+ Thread.Thread.testInterrupt ());
+ val test = check_interrupt_exn (Exn.capture_body main);
val _ = Thread_Attributes.set_attributes orig_atts;
in test end;
@@ -142,11 +178,12 @@
fun try_catch e f =
Thread_Attributes.uninterruptible_body (fn run =>
- run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn);
+ run e () handle exn =>
+ if Exn.is_interrupt exn then Exn.reraise (check_interrupt exn) else f exn);
fun try_finally e f =
Thread_Attributes.uninterruptible_body (fn run =>
- Exn.release (Exn.capture (run e) () before f ()));
+ Exn.release (check_interrupt_exn (Exn.capture_body (run e)) before f ()));
fun try e = Basics.try e ();
fun can e = Basics.can e ();
--- a/src/Pure/Concurrent/lazy.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/lazy.ML Thu Oct 12 21:13:22 2023 +0200
@@ -61,7 +61,7 @@
| Result res => not (Future.is_finished res));
fun is_finished_future res =
- Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res));
+ Future.is_finished res andalso not (Exn.is_interrupt_proper_exn (Future.join_result res));
fun is_finished (Value _) = true
| is_finished (Lazy var) =
@@ -101,11 +101,11 @@
(case expr of
SOME (name, e) =>
let
- val res0 = Exn.capture (run e) ();
- val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
+ val res0 = Exn.capture_body (run e);
+ val _ = Exn.capture_body (fn () => Future.fulfill_result x res0);
val res = Future.get_result x;
val _ =
- if not (Exn.is_interrupt_exn res) then
+ if not (Exn.is_interrupt_proper_exn res) then
Synchronized.assign var (Result (Future.value_result res))
else if strict then
Synchronized.assign var
@@ -114,7 +114,7 @@
interrupt, until there is a fresh start*)
else Synchronized.change var (fn _ => Expr (name, e));
in res end
- | NONE => Exn.capture (run (fn () => Future.join x)) ())
+ | NONE => Exn.capture_body (run (fn () => Future.join x)))
end));
end;
--- a/src/Pure/Concurrent/par_exn.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Thu Oct 12 21:13:22 2023 +0200
@@ -21,10 +21,10 @@
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.is_interrupt*)
+ no occurrences of Par_Exn or Exn.is_interrupt_proper*)
fun par_exns (Par_Exn exns) = exns
- | par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn];
+ | par_exns exn = if Exn.is_interrupt_proper exn then [] else [Exn_Properties.identify [] exn];
fun make exns =
let
@@ -33,14 +33,14 @@
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;
+ | dest exn = if Exn.is_interrupt_proper exn then SOME [] else NONE;
(* parallel results *)
fun is_interrupted results =
exists Exn.is_exn results andalso
- Exn.is_interrupt (make (map_filter Exn.get_exn results));
+ Exn.is_interrupt_proper (make (map_filter Exn.get_exn results));
fun release_all results =
if forall Exn.is_res results
@@ -49,7 +49,7 @@
fun plain_exn (Exn.Res _) = NONE
| plain_exn (Exn.Exn (Par_Exn _)) = NONE
- | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
+ | plain_exn (Exn.Exn exn) = if Exn.is_interrupt_proper exn then NONE else SOME exn;
fun release_first results =
(case get_first plain_exn results of
--- a/src/Pure/Concurrent/task_queue.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Thu Oct 12 21:13:22 2023 +0200
@@ -159,7 +159,7 @@
Thread_Attributes.uninterruptible_body (fn run =>
let
val start = Time.now ();
- val result = Exn.capture (run e) ();
+ val result = Exn.capture_body (run e);
val t = Time.now () - start;
val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
in Exn.release result end);
--- a/src/Pure/Concurrent/timeout.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Concurrent/timeout.ML Thu Oct 12 21:13:22 2023 +0200
@@ -42,13 +42,16 @@
Event_Timer.request {physical = physical} (start + scale_time timeout)
(fn () => Isabelle_Thread.interrupt_other self);
val result =
- Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
+ Exn.capture_body (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x));
val stop = Time.now ();
val was_timeout = not (Event_Timer.cancel request);
val test = Isabelle_Thread.expose_interrupt_result ();
+ val was_interrupt =
+ Exn.is_interrupt_proper_exn result orelse
+ Exn.is_interrupt_proper_exn test;
in
- if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+ if was_timeout andalso was_interrupt
then raise TIMEOUT (stop - start)
else (Exn.release test; Exn.release result)
end);
--- a/src/Pure/General/exn.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/General/exn.ML Thu Oct 12 21:13:22 2023 +0200
@@ -27,7 +27,14 @@
val maps_res: ('a -> 'b result) -> 'a result -> 'b result
val map_exn: (exn -> exn) -> 'a result -> 'a result
val cause: exn -> exn
+ exception Interrupt_Break
+ exception Interrupt_Breakdown
+ val is_interrupt_raw: exn -> bool
+ val is_interrupt_break: exn -> bool
+ val is_interrupt_breakdown: exn -> bool
+ val is_interrupt_proper: exn -> bool
val is_interrupt: exn -> bool
+ val is_interrupt_proper_exn: 'a result -> bool
val is_interrupt_exn: 'a result -> bool
val result: ('a -> 'b) -> 'a -> 'b result
val failure_rc: exn -> int
@@ -39,6 +46,7 @@
sig
include EXN0
val capture: ('a -> 'b) -> 'a -> 'b result (*managed interrupts*)
+ val capture_body: (unit -> 'a) -> 'a result
end;
structure Exn: EXN0 =
@@ -99,10 +107,17 @@
fun cause (IO.Io {cause = exn, ...}) = cause exn
| cause exn = exn;
-fun is_interrupt exn =
- (case cause exn of
- Thread.Thread.Interrupt => true
- | _ => false);
+exception Interrupt_Break;
+exception Interrupt_Breakdown;
+
+fun is_interrupt_raw exn = (case cause exn of Thread.Thread.Interrupt => true | _ => false);
+fun is_interrupt_break exn = (case cause exn of Interrupt_Break => true | _ => false);
+fun is_interrupt_breakdown exn = (case cause exn of Interrupt_Breakdown => true | _ => false);
+fun is_interrupt_proper exn = is_interrupt_raw exn orelse is_interrupt_break exn;
+fun is_interrupt exn = is_interrupt_proper exn orelse is_interrupt_breakdown exn;
+
+fun is_interrupt_proper_exn (Exn exn) = is_interrupt_proper exn
+ | is_interrupt_proper_exn _ = false;
fun is_interrupt_exn (Exn exn) = is_interrupt exn
| is_interrupt_exn _ = false;
--- a/src/Pure/General/http.scala Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/General/http.scala Thu Oct 12 21:13:22 2023 +0200
@@ -243,7 +243,7 @@
val input = using(http.getRequestBody)(Bytes.read_stream(_))
if (http.getRequestMethod == method) {
val request = new Request(server_name, name, uri, input)
- Exn.capture(apply(request)) match {
+ Exn.result(apply(request)) match {
case Exn.Res(Some(response)) =>
response.write(http, 200)
case Exn.Res(None) =>
--- a/src/Pure/General/mercurial.scala Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/General/mercurial.scala Thu Oct 12 21:13:22 2023 +0200
@@ -29,7 +29,7 @@
val server_root = Future.promise[String]
Isabelle_Thread.fork("hg") {
val process =
- Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
+ Exn.result { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
server_process.fulfill_result(process)
Exn.release(process).result(progress_stdout =
line => if (!server_root.is_finished) {
--- a/src/Pure/Isar/runtime.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Isar/runtime.ML Thu Oct 12 21:13:22 2023 +0200
@@ -197,17 +197,16 @@
(f |> debugging opt_context |> Future.interruptible_task
|> ML_Profiling.profile (Options.default_string "profiling")) x;
-fun toplevel_error output_exn f x = f x
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else
+fun toplevel_error output_exn f x =
+ Isabelle_Thread.try_catch (fn () => f x)
+ (fn exn =>
let
val opt_ctxt =
(case Context.get_generic_context () of
NONE => NONE
| SOME context => try Context.proof_of context);
val _ = output_exn (exn_context opt_ctxt exn);
- in raise TOPLEVEL_ERROR end;
+ in raise TOPLEVEL_ERROR end);
fun toplevel_program body =
(body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
--- a/src/Pure/Isar/toplevel.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Oct 12 21:13:22 2023 +0200
@@ -331,7 +331,7 @@
in
fun apply_capture int name markers trans state =
- (case Exn.capture (fn () => apply_body int trans state |> apply_markers name markers) () of
+ (case Exn.capture_body (fn () => apply_body int trans state |> apply_markers name markers) of
Exn.Res res => res
| Exn.Exn exn => (state, SOME exn));
@@ -662,7 +662,7 @@
(case transition int tr st of
(st', NONE) => st'
| (_, SOME (exn, info)) =>
- if Exn.is_interrupt exn then Exn.reraise exn
+ if Exn.is_interrupt_proper exn then Exn.reraise exn
else raise Runtime.EXCURSION_FAIL (exn, info));
val command = command_exception false;
--- a/src/Pure/ML/exn_properties.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/ML/exn_properties.ML Thu Oct 12 21:13:22 2023 +0200
@@ -72,7 +72,7 @@
(* identification via serial numbers *)
fun identify default_props exn =
- if Exn.is_interrupt exn then exn
+ if Exn.is_interrupt_proper exn then exn
else
let
val props = get exn;
--- a/src/Pure/ML/ml_compiler.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/ML/ml_compiler.ML Thu Oct 12 21:13:22 2023 +0200
@@ -299,11 +299,11 @@
PolyML.Compiler.CPBindingSeq serial];
val _ =
- (while not (List.null (! input_buffer)) do
- ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ()))
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else
+ Isabelle_Thread.try_catch
+ (fn () =>
+ (while not (List.null (! input_buffer)) do
+ ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ())))
+ (fn exn =>
let
val exn_msg =
(case exn of
@@ -311,7 +311,7 @@
| Runtime.TOPLEVEL_ERROR => ""
| _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
val _ = err exn_msg;
- in expose_error true end;
+ in expose_error true end);
in expose_error (#verbose flags) end;
end;
--- a/src/Pure/ML/ml_compiler0.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/ML/ml_compiler0.ML Thu Oct 12 21:13:22 2023 +0200
@@ -106,13 +106,13 @@
PolyML.Compiler.CPDebug debug] @
(case print_depth of NONE => [] | SOME d => [PolyML.Compiler.CPPrintDepth (fn () => d)]);
val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else
+ Isabelle_Thread.try_catch
+ (fn () =>
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ()))
+ (fn exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); Exn.reraise exn);
+ error (output ()); Exn.reraise exn));
in if verbose then print (output ()) else () end;
end;
--- a/src/Pure/PIDE/document.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/PIDE/document.ML Thu Oct 12 21:13:22 2023 +0200
@@ -550,7 +550,7 @@
(fn deps => fn (name, node) =>
if Symset.member required name orelse visible_node node orelse pending_result node then
let
- fun body () =
+ fun main () =
(Execution.worker_task_active true name;
if forall finished_import deps then
iterate_entries (fn (_, opt_exec) => fn () =>
@@ -569,7 +569,7 @@
deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
pri = 0, interrupts = false}
(fn () =>
- (case Exn.capture body () of
+ (case Exn.capture_body main of
Exn.Res () => ()
| Exn.Exn exn =>
(Output.system_message (Runtime.exn_message exn);
--- a/src/Pure/PIDE/execution.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/PIDE/execution.ML Thu Oct 12 21:13:22 2023 +0200
@@ -165,11 +165,11 @@
val task = the (Future.worker_task ());
val _ = status task [Markup.running];
val result =
- Exn.capture (Future.interruptible_task e) ()
+ Exn.capture_body (Future.interruptible_task e)
|> Future.identify_result pos
|> Exn.map_exn Runtime.thread_context;
val errors =
- Exn.capture (fn () =>
+ Exn.capture_body (fn () =>
(case result of
Exn.Exn exn =>
(status task [Markup.failed];
@@ -178,7 +178,7 @@
if exec_id = 0 then ()
else List.app (Future.error_message pos) (Runtime.exn_messages exn))
| Exn.Res _ =>
- status task [Markup.finished])) ();
+ status task [Markup.finished]));
val _ = status task [Markup.joined];
in Exn.release errors; Exn.release result end);
--- a/src/Pure/PIDE/protocol.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Oct 12 21:13:22 2023 +0200
@@ -164,7 +164,7 @@
val _ =
Protocol_Command.define "Document.dialog_result"
(fn [serial, result] =>
- (case Exn.capture (fn () => Active.dialog_result (Value.parse_int serial) result) () of
+ (case Exn.capture_body (fn () => Active.dialog_result (Value.parse_int serial) result) of
Exn.Res () => ()
| Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn));
--- a/src/Pure/PIDE/protocol_command.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/PIDE/protocol_command.ML Thu Oct 12 21:13:22 2023 +0200
@@ -40,7 +40,7 @@
(case Symtab.lookup (Synchronized.value commands) name of
NONE => error ("Undefined Isabelle protocol command " ^ quote name)
| SOME cmd =>
- (case Exn.capture (fn () => Runtime.exn_trace_system (fn () => cmd args)) () of
+ (case Exn.capture_body (fn () => Runtime.exn_trace_system (fn () => cmd args)) of
Exn.Res res => res
| Exn.Exn exn =>
if is_protocol_exn exn then Exn.reraise exn
--- a/src/Pure/PIDE/query_operation.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/PIDE/query_operation.ML Thu Oct 12 21:13:22 2023 +0200
@@ -32,7 +32,7 @@
f {state = state, args = args, output_result = output_result,
writeln_result = writeln_result};
val _ =
- (case Exn.capture (*sic!*) (run main) () of
+ (case Exn.capture_body (*sic!*) (run main) of
Exn.Res () => ()
| Exn.Exn exn => toplevel_error exn);
val _ = status Markup.finished;
--- a/src/Pure/System/command_line.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/System/command_line.ML Thu Oct 12 21:13:22 2023 +0200
@@ -12,12 +12,12 @@
structure Command_Line: COMMAND_LINE =
struct
-fun tool body =
+fun tool main =
Thread_Attributes.uninterruptible_body (fn run =>
let
fun print_failure exn = (Runtime.exn_error_message exn; Exn.failure_rc exn);
val rc =
- (case Exn.capture (run body) () of
+ (case Exn.capture_body (run main) of
Exn.Res () => 0
| Exn.Exn exn =>
(case Exn.capture print_failure exn of
--- a/src/Pure/System/isabelle_process.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/System/isabelle_process.ML Thu Oct 12 21:13:22 2023 +0200
@@ -154,13 +154,13 @@
fun protocol_loop () =
let
- fun body () =
+ fun main () =
(case Byte_Message.read_message in_stream of
NONE => raise Protocol_Command.STOP 0
| SOME [] => Output.system_message "Isabelle process: no input"
| SOME (name :: args) => Protocol_Command.run (Bytes.content name) args);
val _ =
- (case Exn.capture body () of
+ (case Exn.capture_body main of
Exn.Res () => ()
| Exn.Exn exn =>
if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
@@ -175,7 +175,7 @@
ml_statistics ();
protocol_loop ());
- val result = Exn.capture (message_context protocol) ();
+ val result = Exn.capture_body (message_context protocol);
(* shutdown *)
--- a/src/Pure/System/isabelle_system.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/System/isabelle_system.ML Thu Oct 12 21:13:22 2023 +0200
@@ -89,7 +89,7 @@
else err ()
| _ => err ())
and loop maybe_uuid s =
- (case Exn.capture (fn () => loop_body s) () of
+ (case Exn.capture_body (fn () => loop_body s) of
Exn.Res res => res
| Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
in
--- a/src/Pure/System/message_channel.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/System/message_channel.ML Thu Oct 12 21:13:22 2023 +0200
@@ -38,8 +38,7 @@
| dispatch (Shutdown :: _) = ()
| dispatch (Message chunks :: rest) =
(Byte_Message.write_message_yxml stream chunks; dispatch rest);
- val thread =
- Isabelle_Thread.fork {name = "message_channel", stack_limit = NONE, interrupts = false} loop;
+ val thread = Isabelle_Thread.fork (Isabelle_Thread.params "message_channel") loop;
in Message_Channel {mbox = mbox, thread = thread} end;
end;
--- a/src/Pure/System/scala.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/System/scala.ML Thu Oct 12 21:13:22 2023 +0200
@@ -60,7 +60,7 @@
| NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
in
invoke ();
- (case Exn.capture (fn () => Exn.release (run await_result ())) () of
+ (case Exn.capture_body (fn () => Exn.release (run await_result ())) of
Exn.Res res => res
| Exn.Exn exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn))
end);
--- a/src/Pure/System/scala.scala Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/System/scala.scala Thu Oct 12 21:13:22 2023 +0200
@@ -289,7 +289,8 @@
case Exn.Res(null) => (Tag.NULL, Nil)
case Exn.Res(res) => (Tag.OK, res)
case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
- case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
+ case Exn.Exn(ERROR(msg)) => (Tag.ERROR, List(Bytes(msg)))
+ case Exn.Exn(e) => (Tag.FAIL, List(Bytes(Exn.message(e))))
}
case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
}
--- a/src/Pure/Thy/thy_info.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Oct 12 21:13:22 2023 +0200
@@ -225,7 +225,7 @@
(case present () of
NONE => []
| SOME (context as {segments, ...}) =>
- [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
+ [Exn.capture_body (fn () => (apply_presentation context theory; (theory, segments)))]);
in
@@ -247,7 +247,7 @@
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
(fn () => body (join_parents deps name parents))
else
- Future.value_result (Exn.capture (fn () => body (join_parents deps name parents)) ())
+ Future.value_result (Exn.capture_body (fn () => body (join_parents deps name parents)))
| Finished theory => Future.value (theory_result theory)));
val results1 = futures |> maps (consolidate_theory o Future.join_result);
@@ -256,7 +256,7 @@
val results2 = (map o Exn.map_res) (K ()) present_results;
val results3 = futures
- |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
+ |> map (fn future => Exn.capture_body (fn () => result_commit (Future.join future) ()));
val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
--- a/src/Pure/Tools/build.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Tools/build.ML Thu Oct 12 21:13:22 2023 +0200
@@ -91,7 +91,7 @@
Exn.Res loaded_theories =>
Exn.capture (apply_hooks session_name) (flat loaded_theories)
| Exn.Exn exn => Exn.Exn exn);
- val res2 = Exn.capture Session.finish ();
+ val res2 = Exn.capture_body Session.finish;
val _ = Resources.finish_session_base ();
val _ = Par_Exn.release_all [res1, res2];
@@ -102,14 +102,12 @@
fun exec e =
if can Theory.get_pure () then
- Isabelle_Thread.fork
- {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
- interrupts = false} e
+ Isabelle_Thread.fork (Isabelle_Thread.params "build_session") e
|> ignore
else e ();
in
exec (fn () =>
- (case Exn.capture (Future.interruptible_task build) () of
+ (case Exn.capture_body (Future.interruptible_task build) of
Exn.Res () => (0, [])
| Exn.Exn exn =>
(case Exn.capture Runtime.exn_message_list exn of
--- a/src/Pure/Tools/simplifier_trace.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Thu Oct 12 21:13:22 2023 +0200
@@ -414,7 +414,7 @@
end
in
fn [serial_string, reply] =>
- (case Exn.capture (fn () => body serial_string reply) () of
+ (case Exn.capture_body (fn () => body serial_string reply) of
Exn.Res () => ()
| Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
end;
--- a/src/Pure/morphism.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/morphism.ML Thu Oct 12 21:13:22 2023 +0200
@@ -83,9 +83,9 @@
exception MORPHISM of string * exn;
-fun app context (name, f) x = f context x
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
+fun app context (name, f) x =
+ Isabelle_Thread.try_catch (fn () => f context x)
+ (fn exn => raise MORPHISM (name, exn));
(* optional context *)
--- a/src/Pure/proofterm.ML Thu Oct 12 12:36:09 2023 +0100
+++ b/src/Pure/proofterm.ML Thu Oct 12 21:13:22 2023 +0200
@@ -2238,14 +2238,16 @@
val open_proof = not named ? rew_proof thy;
+ fun export_body () = join_proof body' |> open_proof |> export_proof thy i prop1;
val export =
if export_enabled () then
Lazy.lazy (fn () =>
- join_proof body' |> open_proof |> export_proof thy i prop1 handle exn =>
- if Exn.is_interrupt exn then
- raise Fail ("Interrupt: potential resource problems while exporting proof " ^
- string_of_int i)
- else Exn.reraise exn)
+ (case Exn.capture_body export_body of
+ Exn.Res res => res
+ | Exn.Exn exn =>
+ if Exn.is_interrupt_breakdown exn then
+ raise Fail ("Resource problems while exporting proof " ^ string_of_int i)
+ else Exn.reraise exn))
else no_export;
val thm_body = prune_body body';