--- a/src/Pure/Concurrent/event_timer.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Wed Oct 11 11:27:01 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 (); (*sic!*)
+ val _ = Exn.capture_body event; (*sic!*)
val state' = make_state (requests', status, manager);
in SOME (true, state') end
| NONE =>
@@ -143,7 +143,7 @@
fun main () =
Synchronized.guarded_access state
(fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE);
- val result = Exn.capture (run main) ();
+ val result = Exn.capture_body (run main);
in
if Exn.is_interrupt_exn result then
Synchronized.change state (fn State {requests, manager, ...} =>
--- a/src/Pure/Concurrent/future.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Oct 11 11:27:01 2023 +0200
@@ -441,9 +441,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;
--- a/src/Pure/Concurrent/isabelle_thread.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Wed Oct 11 11:27:01 2023 +0200
@@ -148,6 +148,7 @@
struct
open Exn;
val capture = capture0;
+ fun capture_body e = capture e ();
end;
fun expose_interrupt_result () =
@@ -156,7 +157,7 @@
fun main () =
(Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
Thread.Thread.testInterrupt ());
- val test = Exn.capture main ();
+ val test = Exn.capture_body main;
val _ = Thread_Attributes.set_attributes orig_atts;
in test end;
@@ -168,7 +169,7 @@
fun try_finally e f =
Thread_Attributes.uninterruptible_body (fn run =>
- Exn.release (Exn.capture (run e) () before f ()));
+ Exn.release (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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML Wed Oct 11 11:27:01 2023 +0200
@@ -101,8 +101,8 @@
(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
@@ -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/task_queue.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML Wed Oct 11 11:27:01 2023 +0200
@@ -42,7 +42,7 @@
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);
--- a/src/Pure/General/exn.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/General/exn.ML Wed Oct 11 11:27:01 2023 +0200
@@ -39,6 +39,7 @@
sig
include EXN0
val capture: ('a -> 'b) -> 'a -> 'b result (*managed interrupts*)
+ val capture_body: (unit -> 'a) -> 'a result
end;
structure Exn: EXN0 =
--- a/src/Pure/Isar/toplevel.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Oct 11 11:27:01 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));
--- a/src/Pure/PIDE/document.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/document.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/execution.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/protocol_command.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/query_operation.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/command_line.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Oct 11 11:27:01 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
--- a/src/Pure/System/isabelle_system.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML Wed Oct 11 11:27:01 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/scala.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/scala.ML Wed Oct 11 11:27:01 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/Thy/thy_info.ML Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Oct 11 11:27:01 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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Tools/build.ML Wed Oct 11 11:27:01 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];
@@ -107,7 +107,7 @@
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 Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Wed Oct 11 11:27:01 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;