--- a/src/Pure/Isar/toplevel.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Sep 28 14:43:07 2023 +0200
@@ -331,8 +331,9 @@
in
fun apply_capture int name markers trans state =
- (apply_body int trans state |> apply_markers name markers)
- handle exn => (state, SOME exn);
+ (case Exn.capture (fn () => apply_body int trans state |> apply_markers name markers) () of
+ Exn.Res res => res
+ | Exn.Exn exn => (state, SOME exn));
end;
--- a/src/Pure/PIDE/command.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/PIDE/command.ML Thu Sep 28 14:43:07 2023 +0200
@@ -193,11 +193,13 @@
in Toplevel.command_errors int tr2 st end
else Toplevel.command_errors int tr st;
+fun check_comments ctxt =
+ Document_Output.check_comments ctxt o Input.source_explode o Token.input_of;
+
fun check_token_comments ctxt tok =
- (Document_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); [])
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else Runtime.exn_messages exn;
+ (case Exn.result (fn () => check_comments ctxt tok) () of
+ Exn.Res () => []
+ | Exn.Exn exn => Runtime.exn_messages exn);
fun check_span_comments ctxt span tr =
Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) ();
@@ -298,11 +300,13 @@
val print_functions =
Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
+fun print_wrapper tr opt_context =
+ Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context;
+
fun print_error tr opt_context e =
- (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn);
+ (case Exn.result (fn () => print_wrapper tr opt_context e ()) () of
+ Exn.Res res => res
+ | Exn.Exn exn => List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn));
fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
--- a/src/Pure/PIDE/document.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/PIDE/document.ML Thu Sep 28 14:43:07 2023 +0200
@@ -550,6 +550,18 @@
(fn deps => fn (name, node) =>
if Symset.member required name orelse visible_node node orelse pending_result node then
let
+ fun body () =
+ (Execution.worker_task_active true name;
+ if forall finished_import deps then
+ iterate_entries (fn (_, opt_exec) => fn () =>
+ (case opt_exec of
+ SOME exec =>
+ if Execution.is_running execution_id
+ then SOME (Command.exec execution_id exec)
+ else NONE
+ | NONE => NONE)) node ()
+ else ();
+ Execution.worker_task_active false name);
val future =
(singleton o Future.forks)
{name = "theory:" ^ name,
@@ -557,21 +569,12 @@
deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
pri = 0, interrupts = false}
(fn () =>
- (Execution.worker_task_active true name;
- if forall finished_import deps then
- iterate_entries (fn (_, opt_exec) => fn () =>
- (case opt_exec of
- SOME exec =>
- if Execution.is_running execution_id
- then SOME (Command.exec execution_id exec)
- else NONE
- | NONE => NONE)) node ()
- else ();
- Execution.worker_task_active false name)
- handle exn =>
+ (case Exn.capture body () of
+ Exn.Res () => ()
+ | Exn.Exn exn =>
(Output.system_message (Runtime.exn_message exn);
Execution.worker_task_active false name;
- Exn.reraise exn));
+ Exn.reraise exn)));
in (node, SOME (Future.task_of future)) end
else (node, NONE));
val execution' =
--- a/src/Pure/PIDE/protocol.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu Sep 28 14:43:07 2023 +0200
@@ -164,8 +164,9 @@
val _ =
Protocol_Command.define "Document.dialog_result"
(fn [serial, result] =>
- Active.dialog_result (Value.parse_int serial) result
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
+ (case Exn.capture (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));
val _ =
Protocol_Command.define "ML_Heap.full_gc"
--- a/src/Pure/PIDE/protocol_command.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/PIDE/protocol_command.ML Thu Sep 28 14:43:07 2023 +0200
@@ -40,8 +40,9 @@
(case Symtab.lookup (Synchronized.value commands) name of
NONE => error ("Undefined Isabelle protocol command " ^ quote name)
| SOME cmd =>
- (Runtime.exn_trace_system (fn () => cmd args)
- handle exn =>
+ (case Exn.capture (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
else error ("Isabelle protocol command failure: " ^ quote name)));
--- a/src/Pure/System/command_line.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/System/command_line.ML Thu Sep 28 14:43:07 2023 +0200
@@ -15,9 +15,14 @@
fun tool body =
Thread_Attributes.uninterruptible_body (fn run =>
let
+ fun print_failure exn = (Runtime.exn_error_message exn; Exn.failure_rc exn);
val rc =
- (run body (); 0) handle exn =>
- ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
+ (case Exn.capture (run body) () of
+ Exn.Res () => 0
+ | Exn.Exn exn =>
+ (case Exn.capture print_failure exn of
+ Exn.Res rc => rc
+ | Exn.Exn crash => Exn.failure_rc crash));
in exit rc end);
end;
--- a/src/Pure/System/isabelle_process.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/System/isabelle_process.ML Thu Sep 28 14:43:07 2023 +0200
@@ -154,14 +154,20 @@
fun protocol_loop () =
let
- val _ =
+ fun body () =
(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)
- handle exn =>
- if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
- else (Runtime.exn_system_message exn handle crash => recover crash);
+ | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args);
+ val _ =
+ (case Exn.capture body () of
+ Exn.Res () => ()
+ | Exn.Exn exn =>
+ if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
+ else
+ (case Exn.capture Runtime.exn_system_message exn of
+ Exn.Res () => ()
+ | Exn.Exn crash => recover crash));
in protocol_loop () end;
fun protocol () =
--- a/src/Pure/System/isabelle_system.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML Thu Sep 28 14:43:07 2023 +0200
@@ -62,7 +62,7 @@
Thread_Attributes.uninterruptible_body (fn run =>
let
fun err () = raise Fail "Malformed result from bash_process server";
- fun loop maybe_uuid s =
+ fun loop_body s =
(case run Byte_Message.read_message_string (#1 s) of
SOME (head :: args) =>
if head = Bash.server_uuid andalso length args = 1 then
@@ -88,7 +88,10 @@
end
else err ()
| _ => err ())
- handle exn => (kill maybe_uuid; Exn.reraise exn);
+ and loop maybe_uuid s =
+ (case Exn.capture (fn () => loop_body s) () of
+ Exn.Res res => res
+ | Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
in
with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
end)
--- a/src/Pure/System/scala.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/System/scala.ML Thu Sep 28 14:43:07 2023 +0200
@@ -60,8 +60,9 @@
| NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
in
invoke ();
- Exn.release (run await_result ())
- handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
+ (case Exn.capture (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);
val function1_bytes = singleton o function_bytes;
--- a/src/Pure/Tools/build.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/Tools/build.ML Thu Sep 28 14:43:07 2023 +0200
@@ -109,8 +109,12 @@
else e ();
in
exec (fn () =>
- (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn =>
- ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
+ (case Exn.capture (Future.interruptible_task build) () of
+ Exn.Res () => (0, [])
+ | Exn.Exn exn =>
+ (case Exn.capture Runtime.exn_message_list exn of
+ Exn.Res errs => (1, errs)
+ | Exn.Exn _ (*sic!*) => (2, ["CRASHED"])))
|> let open XML.Encode in pair int (list string) end
|> single
|> Output.protocol_message Markup.build_session_finished)
--- a/src/Pure/Tools/debugger.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/Tools/debugger.ML Thu Sep 28 14:43:07 2023 +0200
@@ -29,10 +29,10 @@
val warning_message = output_message Markup.warningN;
val error_message = output_message Markup.errorN;
-fun error_wrapper e = e ()
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else error_message (Runtime.exn_message exn);
+fun error_wrapper e =
+ (case Exn.result e () of
+ Exn.Res res => res
+ | Exn.Exn exn => error_message (Runtime.exn_message exn));
(* thread input *)
--- a/src/Pure/Tools/simplifier_trace.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Thu Sep 28 14:43:07 2023 +0200
@@ -400,17 +400,24 @@
val _ =
Protocol_Command.define "Simplifier_Trace.reply"
- (fn [serial_string, reply] =>
- let
- val serial = Value.parse_int serial_string
- val result =
- Synchronized.change_result futures
- (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
- in
- (case result of
- SOME promise => Future.fulfill promise reply
- | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
- end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
+ let
+ fun body serial_string reply =
+ let
+ val serial = Value.parse_int serial_string
+ val result =
+ Synchronized.change_result futures
+ (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
+ in
+ (case result of
+ SOME promise => Future.fulfill promise reply
+ | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
+ end
+ in
+ fn [serial_string, reply] =>
+ (case Exn.capture (fn () => body serial_string reply) () of
+ Exn.Res () => ()
+ | Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
+ end;