# HG changeset patch # User wenzelm # Date 1695904987 -7200 # Node ID 3c02ad5a15864f96b525f4192a4a6f0671e3f7a6 # Parent f2d7f4334cdc10cc30610f80a8e2a0fcbd24aa37 clarified treatment of exceptions: avoid catch-all handlers; diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/Isar/toplevel.ML --- 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; diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/PIDE/command.ML --- 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; diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/PIDE/document.ML --- 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' = diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/PIDE/protocol.ML --- 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" diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/PIDE/protocol_command.ML --- 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))); diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/System/command_line.ML --- 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; diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/System/isabelle_process.ML --- 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 () = diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/System/isabelle_system.ML --- 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) diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/System/scala.ML --- 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; diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/Tools/build.ML --- 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) diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/Tools/debugger.ML --- 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 *) diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/Tools/simplifier_trace.ML --- 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;