--- a/NEWS Wed Sep 27 13:34:15 2023 +0100
+++ b/NEWS Fri Sep 29 11:19:43 2023 +0200
@@ -14,6 +14,26 @@
before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
+*** ML ***
+
+* ML antiquotation "try" provides variants of exception handling that
+avoids accidental capture of physical interrupts (which could affect ML
+semantics in unpredictable ways):
+
+ \<^try>\<open>EXPR catch HANDLER\<close>
+ \<^try>\<open>EXPR finally HANDLER\<close>
+ \<^try>\<open>EXPR\<close>
+
+See also the implementations Isabelle_Thread.try_catch / try_finally /
+try. The HANDLER always runs as uninterruptible, but the EXPR uses the
+the current thread attributes (normally interruptible). Various examples
+occur in the Isabelle sources (.ML and .thy files).
+
+* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
+INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
+as last resort declare [[ML_catch_all]] within the theory context.
+
+
New in Isabelle2023 (September 2023)
------------------------------------
--- a/src/Doc/Implementation/ML.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Sep 29 11:19:43 2023 +0200
@@ -1958,7 +1958,7 @@
\begin{mldecls}
@{define_ML_type 'a "Exn.result"} \\
@{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
- @{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+ @{define_ML Exn.result: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
@{define_ML Exn.release: "'a Exn.result -> 'a"} \\
@{define_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
@{define_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
@@ -1973,8 +1973,8 @@
precautions apply to user code: interrupts must not be absorbed
accidentally!
- \<^descr> \<^ML>\<open>Exn.interruptible_capture\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but
- interrupts are immediately re-raised as required for user code.
+ \<^descr> \<^ML>\<open>Exn.result\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but interrupts are
+ immediately re-raised as required for user code.
\<^descr> \<^ML>\<open>Exn.release\<close>~\<open>result\<close> releases the original runtime result, exposing
its regular value or raising the reified exception.
--- a/src/HOL/Library/code_test.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Library/code_test.ML Fri Sep 29 11:19:43 2023 +0200
@@ -141,8 +141,7 @@
fun with_debug_dir name f =
(Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
|> Isabelle_System.make_directory
- |> Exn.capture f
- |> Exn.release;
+ |> f
fun dynamic_value_strict ctxt t compiler =
let
@@ -157,8 +156,7 @@
(driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result))
|> parse_result compiler
fun evaluator program _ vs_ty deps =
- Exn.interruptible_capture eval
- (Code_Target.compilation_text ctxt target program deps true vs_ty)
+ Exn.result eval (Code_Target.compilation_text ctxt target program deps true vs_ty)
fun postproc f = map (apsnd (Option.map (map f)))
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
@@ -313,8 +311,8 @@
val _ = File.write driver_path driver
val _ =
ML_Context.eval
- {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
- writeln = writeln, warning = warning}
+ {environment = ML_Env.SML, redirect = false, verbose = false, catch_all = true,
+ debug = NONE, writeln = writeln, warning = warning}
Position.none
(ML_Lex.read_text (code, Position.file (File.symbolic_path code_path)) @
ML_Lex.read_text (driver, Position.file (File.symbolic_path driver_path)) @
--- a/src/HOL/Matrix_LP/Cplex_tools.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML Fri Sep 29 11:19:43 2023 +0200
@@ -1150,15 +1150,17 @@
val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
val answer = #1 (Isabelle_System.bash_output command)
in
- let
- val result = load_glpkResult resultname
- val _ = OS.FileSys.remove lpname
- val _ = OS.FileSys.remove resultname
- in
- result
- end
- handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
- | exn => if Exn.is_interrupt exn then Exn.reraise exn else raise (Execute answer)
+ \<^try>\<open>
+ let
+ val result = load_glpkResult resultname
+ val _ = OS.FileSys.remove lpname
+ val _ = OS.FileSys.remove resultname
+ in
+ result
+ end
+ catch Load_cplexResult s => raise Execute ("Load_cplexResult: "^s^"\nExecute: "^answer)
+ | _ => raise Execute answer
+ \<close>
end
fun solve_cplex prog =
--- a/src/HOL/Metis.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Metis.thy Fri Sep 29 11:19:43 2023 +0200
@@ -10,7 +10,10 @@
imports ATP
begin
-ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+context notes [[ML_catch_all]]
+begin
+ ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+end
subsection \<open>Literal selection and lambda-lifting helpers\<close>
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Sep 29 11:19:43 2023 +0200
@@ -157,21 +157,23 @@
(Global_Theory.all_thms_of thy true)
fun check_formulas tsp =
- let
- fun is_type_actually_monotonic T =
- Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
- val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
- val (mono_free_Ts, nonmono_free_Ts) =
- Timeout.apply mono_timeout
- (List.partition is_type_actually_monotonic) free_Ts
- in
- if not (null mono_free_Ts) then "MONO"
- else if not (null nonmono_free_Ts) then "NONMONO"
- else "NIX"
- end
- handle Timeout.TIMEOUT _ => "TIMEOUT"
- | NOT_SUPPORTED _ => "UNSUP"
- | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
+ \<^try>\<open>
+ let
+ fun is_type_actually_monotonic T =
+ Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
+ val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
+ val (mono_free_Ts, nonmono_free_Ts) =
+ Timeout.apply mono_timeout
+ (List.partition is_type_actually_monotonic) free_Ts
+ in
+ if not (null mono_free_Ts) then "MONO"
+ else if not (null nonmono_free_Ts) then "NONMONO"
+ else "NIX"
+ end
+ catch Timeout.TIMEOUT _ => "TIMEOUT"
+ | NOT_SUPPORTED _ => "UNSUP"
+ | _ => "UNKNOWN"
+ \<close>
fun check_theory thy =
let
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Sep 29 11:19:43 2023 +0200
@@ -75,6 +75,11 @@
tptp_informative_failure = true
]]
+ML \<open>
+exception UNSUPPORTED_ROLE
+exception INTERPRET_INFERENCE
+\<close>
+
ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
ML "open TPTP_Reconstruct_Library"
ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>
@@ -867,16 +872,18 @@
SOME (rev acc)
else NONE
else
- let
- val (arg_ty, val_ty) = Term.dest_funT cur_ty
- (*now find a param of type arg_ty*)
- val (candidate_param, params') =
- find_and_remove (snd #> pair arg_ty #> (op =)) params
- in
- use_candidate target_ty params' (candidate_param :: acc) val_ty
- end
- handle TYPE ("dest_funT", _, _) => NONE (* FIXME fragile *)
+ \<^try>\<open>
+ let
+ val (arg_ty, val_ty) = Term.dest_funT cur_ty
+ (*now find a param of type arg_ty*)
+ val (candidate_param, params') =
+ find_and_remove (snd #> pair arg_ty #> (op =)) params
+ in
+ use_candidate target_ty params' (candidate_param :: acc) val_ty
+ end
+ catch TYPE ("dest_funT", _, _) => NONE (* FIXME fragile *)
| _ => NONE (* FIXME avoid catch-all handler *)
+ \<close>
val (skolem_const_ty, params') = skolem_const_info_of conclusion
@@ -2012,9 +2019,6 @@
subsection "Leo2 reconstruction tactic"
ML \<open>
-exception UNSUPPORTED_ROLE
-exception INTERPRET_INFERENCE
-
(*Failure reports can be adjusted to avoid interrupting
an overall reconstruction process*)
fun fail ctxt x =
--- a/src/HOL/TPTP/TPTP_Test.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy Fri Sep 29 11:19:43 2023 +0200
@@ -56,15 +56,11 @@
let
val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
in
- (f file_name; ())
+ \<^try>\<open>(f file_name; ()) catch exn =>
(*otherwise report exceptions as warnings*)
- handle exn =>
- if Exn.is_interrupt exn then
- Exn.reraise exn
- else
- (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
- " raised exception: " ^ Runtime.exn_message exn);
- default_val)
+ (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
+ " raised exception: " ^ Runtime.exn_message exn);
+ default_val)\<close>
end
fun timed_test ctxt f test_files =
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Fri Sep 29 11:19:43 2023 +0200
@@ -95,9 +95,7 @@
| exn => "exception: " ^ General.exnMessage exn);
fun run_action_function f =
- f () handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else print_exn exn;
+ \<^try>\<open>f () catch exn => print_exn exn\<close>;
fun make_action_path ({index, label, name, ...} : action_context) =
Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Sep 29 11:19:43 2023 +0200
@@ -273,31 +273,32 @@
local
fun run_sh params keep pos state =
- let
- fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
- let
- val filename = "prob_" ^
- StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
- StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
- in
- Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
- #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
- #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
- #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
- end
- | set_file_name NONE = I
- val state' = state
- |> Proof.map_context (set_file_name keep)
+ \<^try>\<open>
+ let
+ fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
+ let
+ val filename = "prob_" ^
+ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
+ StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
+ in
+ Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
+ #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
+ #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
+ #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+ end
+ | set_file_name NONE = I
+ val state' = state
+ |> Proof.map_context (set_file_name keep)
- val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
- Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
- Sledgehammer_Fact.no_fact_override state') ()
- in
- (sledgehammer_outcome, msg, cpu_time)
- end
- handle
- ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
- | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
+ val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
+ Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
+ Sledgehammer_Fact.no_fact_override state') ()
+ in
+ (sledgehammer_outcome, msg, cpu_time)
+ end
+ catch ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
+ | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
+ \<close>
in
--- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Sep 29 11:19:43 2023 +0200
@@ -1006,23 +1006,25 @@
if overlord then ()
else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
in
- let
- val _ = File.write kki_path kki
- val rc =
- Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
- \\"$KODKODI/bin/kodkodi\"" ^
- (" -max-msecs " ^ string_of_int timeout) ^
- (if solve_all then " -solve-all" else "") ^
- " -max-solutions " ^ string_of_int max_solutions ^
- (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
- " < " ^ File.bash_path kki_path ^
- " > " ^ File.bash_path out_path ^
- " 2> " ^ File.bash_path err_path)
- val out = File.read out_path
- val err = File.read err_path
- val _ = remove_temporary_files ()
- in (rc, out, err) end
- handle exn => (remove_temporary_files (); Exn.reraise exn)
+ \<^try>\<open>
+ let
+ val _ = File.write kki_path kki
+ val rc =
+ Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
+ \\"$KODKODI/bin/kodkodi\"" ^
+ (" -max-msecs " ^ string_of_int timeout) ^
+ (if solve_all then " -solve-all" else "") ^
+ " -max-solutions " ^ string_of_int max_solutions ^
+ (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
+ " < " ^ File.bash_path kki_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path)
+ val out = File.read out_path
+ val err = File.read err_path
+ val _ = remove_temporary_files ()
+ in (rc, out, err) end
+ finally remove_temporary_files ()
+ \<close>
end
else
(timeout, (solve_all, (max_solutions, (max_threads, kki))))
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Sep 29 11:19:43 2023 +0200
@@ -211,8 +211,7 @@
fun with_overlord_dir name f =
(Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
|> Isabelle_System.make_directory
- |> Exn.capture f
- |> Exn.release
+ |> f
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
ctxt cookie (code_modules_bytes, _) =
@@ -315,7 +314,7 @@
fun dynamic_value_strict opts cookie ctxt postproc t =
let
fun evaluator program _ vs_ty_t deps =
- Exn.interruptible_capture (value opts ctxt cookie)
+ Exn.result (value opts ctxt cookie)
(Code_Target.compilation_text ctxt target program deps true vs_ty_t)
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 29 11:19:43 2023 +0200
@@ -328,12 +328,9 @@
if debug then
really_go ()
else
- (really_go ()
- handle
- ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
- | exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n"))
+ \<^try>\<open>really_go ()
+ catch ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
+ | exn => (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n")\<close>
val (outcome, message) = Timeout.apply hard_timeout go ()
val () = check_expected_outcome ctxt prover_name expect outcome
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Sep 29 11:19:43 2023 +0200
@@ -578,20 +578,17 @@
handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *)
fun try_graph ctxt when def f =
- f ()
- handle
- Graph.CYCLES (cycle :: _) =>
- (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
- | Graph.DUP name =>
- (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
- | Graph.UNDEF name =>
- (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
- | exn =>
- if Exn.is_interrupt exn then
- Exn.reraise exn
- else
- (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
- def)
+ \<^try>\<open>f ()
+ catch
+ Graph.CYCLES (cycle :: _) =>
+ (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
+ | Graph.DUP name =>
+ (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
+ | Graph.UNDEF name =>
+ (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
+ | exn =>
+ (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
+ def)\<close>
fun graph_info G =
string_of_int (length (Graph.keys G)) ^ " node(s), " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Sep 29 11:19:43 2023 +0200
@@ -279,7 +279,7 @@
(output, run_time, used_from, atp_problem, tstplike_proof, atp_proof,
atp_abduce_candidates, outcome),
(format, type_enc)) =
- with_cleanup clean_up run () |> tap export
+ \<^try>\<open>run () finally clean_up ()\<close> |> tap export
val (outcome, used_facts, preferred_methss, message) =
(case outcome of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Sep 29 11:19:43 2023 +0200
@@ -104,13 +104,10 @@
val birth = Timer.checkRealTimer timer
val filter_result as {outcome, ...} =
- SMT_Solver.smt_filter ctxt goal facts i run_timeout options
- handle exn =>
- if Exn.is_interrupt exn orelse debug then
- Exn.reraise exn
- else
- {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
- atp_proof = K []}
+ \<^try>\<open>SMT_Solver.smt_filter ctxt goal facts i run_timeout options
+ catch exn =>
+ {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
+ atp_proof = K []}\<close>
val death = Timer.checkRealTimer timer
val run_time = death - birth
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 29 11:19:43 2023 +0200
@@ -12,7 +12,6 @@
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
- val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
val parse_bool_option : bool -> string -> string -> bool option
val parse_time : string -> string -> Time.time
val subgoal_count : Proof.state -> int
@@ -42,11 +41,6 @@
val serial_commas = Try.serial_commas
val simplify_spaces = strip_spaces false (K true)
-fun with_cleanup clean_up f x =
- Exn.capture f x
- |> tap (fn _ => clean_up x)
- |> Exn.release
-
fun parse_bool_option option name s =
(case s of
"smart" => if option then NONE else raise Option.Option
--- a/src/Pure/Concurrent/event_timer.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/event_timer.ML Fri Sep 29 11:19:43 2023 +0200
@@ -134,14 +134,14 @@
manager_loop);
fun shutdown () =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
if is_shutdown Normal st then (false, st)
else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
raise Fail "Concurrent attempt to shutdown event timer"
else (true, make_state (requests, Shutdown_Req, manager_check manager)))
then
- restore_attributes (fn () =>
+ run (fn () =>
Synchronized.guarded_access state
(fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) ()
handle exn =>
@@ -149,7 +149,7 @@
Synchronized.change state (fn State {requests, manager, ...} =>
make_state (requests, Normal, manager))
else ()
- else ()) ();
+ else ());
(* main operations *)
@@ -170,12 +170,12 @@
in (canceled, make_state (requests', status, manager')) end);
fun future physical time =
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
let
val req: request Single_Assignment.var = Single_Assignment.var "req";
fun abort () = ignore (cancel (Single_Assignment.await req));
val promise: unit future = Future.promise_name "event_timer" abort;
val _ = Single_Assignment.assign req (request physical time (Future.fulfill promise));
- in promise end) ();
+ in promise end);
end;
--- a/src/Pure/Concurrent/future.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Sep 29 11:19:43 2023 +0200
@@ -214,7 +214,7 @@
then Thread_Attributes.private_interrupts
else Thread_Attributes.public_interrupts)
(fn _ => f x)
- before Thread_Attributes.expose_interrupt ();
+ before Isabelle_Thread.expose_interrupt ();
(* worker threads *)
@@ -234,7 +234,7 @@
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
- val test = Exn.capture Thread_Attributes.expose_interrupt ();
+ val test = Isabelle_Thread.expose_interrupt_result ();
val _ =
if ok andalso not (Exn.is_interrupt_exn test) then ()
else if null (cancel_now group) then ()
@@ -550,7 +550,7 @@
(* forked results: nested parallel evaluation *)
fun forked_results {name, deps} es =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val (group, pri) =
(case worker_task () of
@@ -560,9 +560,9 @@
val futures =
forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
in
- restore_attributes join_results futures
+ run join_results futures
handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
- end) ();
+ end);
(* task context for running thread *)
@@ -614,10 +614,10 @@
fun cond_forks args es =
if enabled () then forks args es
- else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+ else map (fn e => value_result (Exn.result e ())) es;
fun map_future f x =
- if is_finished x then value_result (Exn.interruptible_capture (f o join) x)
+ if is_finished x then value_result (Exn.result (f o join) x)
else
let
val task = task_of x;
--- a/src/Pure/Concurrent/isabelle_thread.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.ML Fri Sep 29 11:19:43 2023 +0200
@@ -14,6 +14,7 @@
val print: T -> string
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 attributes: params -> Thread.Thread.threadAttribute list
@@ -24,6 +25,11 @@
val interrupt_exn: 'a Exn.result
val interrupt_self: unit -> 'a
val interrupt_other: T -> unit
+ structure Exn: EXN
+ val expose_interrupt_result: unit -> unit Exn.result
+ val expose_interrupt: unit -> unit (*exception Interrupt*)
+ val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
+ val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
val try: (unit -> 'a) -> 'a option
val can: (unit -> 'a) -> bool
end;
@@ -43,11 +49,11 @@
val get_name = #name o dest;
val get_id = #id o dest;
-val equal = Thread.Thread.equal o apply2 get_thread;
+fun equal (t1, t2) = Thread.Thread.equal (get_thread t1, get_thread t2);
fun print t =
(case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^
- "-" ^ string_of_int (get_id t);
+ "-" ^ Int.toString (get_id t);
(* self *)
@@ -73,11 +79,12 @@
(* fork *)
+val threads_stack_limit = Unsynchronized.ref 0.25;
+
fun stack_limit () =
let
- val threads_stack_limit =
- Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
- in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;
+ 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};
@@ -117,7 +124,33 @@
fun interrupt_other t =
Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
+structure Exn: EXN =
+struct
+ open Exn;
+ val capture = capture0;
+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 ();
+ val _ = Thread_Attributes.set_attributes orig_atts;
+ in test end;
+
+val expose_interrupt = Exn.release o expose_interrupt_result;
+
+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);
+
+fun try_finally e f =
+ Thread_Attributes.uninterruptible_body (fn run =>
+ Exn.release (Exn.capture (run e) () before f ()));
+
fun try e = Basics.try e ();
fun can e = Basics.can e ();
end;
+
+structure Exn = Isabelle_Thread.Exn;
--- a/src/Pure/Concurrent/lazy.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/lazy.ML Fri Sep 29 11:19:43 2023 +0200
@@ -85,7 +85,7 @@
(case peek (Lazy var) of
SOME res => res
| NONE =>
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val (expr, x) =
Synchronized.change_result var
@@ -101,7 +101,7 @@
(case expr of
SOME (name, e) =>
let
- val res0 = Exn.capture (restore_attributes e) ();
+ val res0 = Exn.capture (run e) ();
val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
val res = Future.get_result x;
val _ =
@@ -114,8 +114,8 @@
interrupt, until there is a fresh start*)
else Synchronized.change var (fn _ => Expr (name, e));
in res end
- | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
- end) ());
+ | NONE => Exn.capture (run (fn () => Future.join x)) ())
+ end));
end;
--- a/src/Pure/Concurrent/multithreading.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/multithreading.ML Fri Sep 29 11:19:43 2023 +0200
@@ -67,9 +67,9 @@
fun tracing level msg =
if ! trace < level then ()
- else Thread_Attributes.uninterruptible (fn _ => fn () =>
+ else Thread_Attributes.uninterruptible_body (fn _ =>
(TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
- handle _ (*sic*) => ()) ();
+ handle _ (*sic*) => ());
fun tracing_time detailed time =
tracing
@@ -83,7 +83,7 @@
(* synchronized evaluation *)
fun synchronized name lock e =
- Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Exn.release (Thread_Attributes.uninterruptible_body (fn run =>
if ! trace > 0 then
let
val immediate =
@@ -96,15 +96,15 @@
val time = Timer.checkRealTimer timer;
val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
in false end;
- val result = Exn.capture (restore_attributes e) ();
+ val result = Exn.capture0 (run e) ();
val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
val _ = Thread.Mutex.unlock lock;
in result end
else
let
val _ = Thread.Mutex.lock lock;
- val result = Exn.capture (restore_attributes e) ();
+ val result = Exn.capture0 (run e) ();
val _ = Thread.Mutex.unlock lock;
- in result end) ());
+ in result end));
end;
--- a/src/Pure/Concurrent/par_list.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/par_list.ML Fri Sep 29 11:19:43 2023 +0200
@@ -37,7 +37,7 @@
fun map' params f xs = Par_Exn.release_first (managed_results params f xs);
fun map f = map' {name = "", sequential = false} f;
-fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
+fun map_independent f = map (Exn.result f) #> Par_Exn.release_all;
fun get_some f xs =
let
--- a/src/Pure/Concurrent/single_assignment.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/single_assignment.ML Fri Sep 29 11:19:43 2023 +0200
@@ -61,9 +61,9 @@
(case ! state of
Set _ => assign_fail name
| Unset _ =>
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
(state := Set x; RunCall.clearMutableBit state;
- Thread.ConditionVar.broadcast cond)) ())));
+ Thread.ConditionVar.broadcast cond)))));
end;
--- a/src/Pure/Concurrent/synchronized.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/synchronized.ML Fri Sep 29 11:19:43 2023 +0200
@@ -57,9 +57,9 @@
(case ! state of
Immutable _ => immutable_fail name
| Mutable _ =>
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
(state := Immutable x; RunCall.clearMutableBit state;
- Thread.ConditionVar.broadcast cond)) ())));
+ Thread.ConditionVar.broadcast cond)))));
(* synchronized access *)
@@ -81,9 +81,9 @@
| Exn.Res false => NONE
| Exn.Exn exn => Exn.reraise exn)
| SOME (y, x') =>
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
(state := Mutable {lock = lock, cond = cond, content = x'};
- Thread.ConditionVar.broadcast cond; SOME y)) ()));
+ Thread.ConditionVar.broadcast cond; SOME y))));
in try_change () end));
fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
--- a/src/Pure/Concurrent/task_queue.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Fri Sep 29 11:19:43 2023 +0200
@@ -156,13 +156,13 @@
fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
fun update_timing update (Task {timing, ...}) e =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val start = Time.now ();
- val result = Exn.capture (restore_attributes e) ();
+ val result = Exn.capture (run e) ();
val t = Time.now () - start;
val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
- in Exn.release result end) ();
+ in Exn.release result end);
fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
--- a/src/Pure/Concurrent/thread_attributes.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/thread_attributes.ML Fri Sep 29 11:19:43 2023 +0200
@@ -18,7 +18,7 @@
val safe_interrupts: attributes -> attributes
val with_attributes: attributes -> (attributes -> 'a) -> 'a
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
- val expose_interrupt: unit -> unit (*exception Interrupt*)
+ val uninterruptible_body: ((('b -> 'c) -> 'b -> 'c) -> 'a) -> 'a
end;
structure Thread_Attributes: THREAD_ATTRIBUTES =
@@ -96,7 +96,7 @@
if atts1 = atts2 then e atts1
else
let
- val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
+ val result = Exn.capture0 (fn () => (set_attributes atts2; e atts1)) ();
val _ = set_attributes atts1;
in Exn.release result end
end;
@@ -107,12 +107,7 @@
with_attributes no_interrupts (fn atts =>
f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-fun expose_interrupt () =
- let
- val orig_atts = safe_interrupts (get_attributes ());
- val _ = set_attributes test_interrupts;
- val test = Exn.capture Thread.Thread.testInterrupt ();
- val _ = set_attributes orig_atts;
- in Exn.release test end;
+fun uninterruptible_body body =
+ uninterruptible (fn run => fn () => body run) ();
end;
--- a/src/Pure/Concurrent/thread_data.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/thread_data.ML Fri Sep 29 11:19:43 2023 +0200
@@ -30,13 +30,13 @@
fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
fun setmp v data f x =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val orig_data = get v;
val _ = put v data;
- val result = Exn.capture (restore_attributes f) x;
+ val result = Exn.capture0 (run f) x;
val _ = put v orig_data;
- in Exn.release result end) ();
+ in Exn.release result end);
end;
--- a/src/Pure/Concurrent/thread_data_virtual.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/thread_data_virtual.ML Fri Sep 29 11:19:43 2023 +0200
@@ -30,13 +30,13 @@
| SOME x => Inttab.update (i, Universal.tagInject tag x));
fun setmp v data f x =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val orig_data = get v;
val _ = put v data;
- val result = Exn.capture (restore_attributes f) x;
+ val result = Exn.capture (run f) x;
val _ = put v orig_data;
- in Exn.release result end) ();
+ in Exn.release result end);
end;
--- a/src/Pure/Concurrent/timeout.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/timeout.ML Fri Sep 29 11:19:43 2023 +0200
@@ -46,7 +46,7 @@
val stop = Time.now ();
val was_timeout = not (Event_Timer.cancel request);
- val test = Exn.capture Thread_Attributes.expose_interrupt ();
+ val test = Isabelle_Thread.expose_interrupt_result ();
in
if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
then raise TIMEOUT (stop - start)
--- a/src/Pure/Concurrent/unsynchronized.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/unsynchronized.ML Fri Sep 29 11:19:43 2023 +0200
@@ -39,13 +39,13 @@
fun add i n = (i := ! i + (n: int); ! i);
fun setmp flag value f x =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val orig_value = ! flag;
val _ = flag := value;
- val result = Exn.capture (restore_attributes f) x;
+ val result = Exn.capture0 (run f) x;
val _ = flag := orig_value;
- in Exn.release result end) ();
+ in Exn.release result end);
(* weak references *)
--- a/src/Pure/General/exn.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/exn.ML Fri Sep 29 11:19:43 2023 +0200
@@ -11,7 +11,7 @@
val cat_error: string -> string -> 'a
end;
-signature EXN =
+signature EXN0 =
sig
include BASIC_EXN
val polyml_location: exn -> PolyML.location option
@@ -21,7 +21,7 @@
val is_exn: 'a result -> bool
val get_res: 'a result -> 'a option
val get_exn: 'a result -> exn option
- val capture: ('a -> 'b) -> 'a -> 'b result
+ val capture0: ('a -> 'b) -> 'a -> 'b result (*unmanaged interrupts*)
val release: 'a result -> 'a
val map_res: ('a -> 'b) -> 'a result -> 'b result
val maps_res: ('a -> 'b result) -> 'a result -> 'b result
@@ -29,13 +29,19 @@
val cause: exn -> exn
val is_interrupt: exn -> bool
val is_interrupt_exn: 'a result -> bool
- val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+ val result: ('a -> 'b) -> 'a -> 'b result
val failure_rc: exn -> int
exception EXCEPTIONS of exn list
val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
end;
-structure Exn: EXN =
+signature EXN =
+sig
+ include EXN0
+ val capture: ('a -> 'b) -> 'a -> 'b result (*managed interrupts*)
+end;
+
+structure Exn: EXN0 =
struct
(* location *)
@@ -74,7 +80,7 @@
fun get_exn (Exn exn) = SOME exn
| get_exn _ = NONE;
-fun capture f x = Res (f x) handle e => Exn e;
+fun capture0 f x = Res (f x) handle e => Exn e;
fun release (Res y) = y
| release (Exn e) = reraise e;
@@ -101,7 +107,7 @@
fun is_interrupt_exn (Exn exn) = is_interrupt exn
| is_interrupt_exn _ = false;
-fun interruptible_capture f x =
+fun result f x =
Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
fun failure_rc exn = if is_interrupt exn then 130 else 2;
--- a/src/Pure/General/exn.scala Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/exn.scala Fri Sep 29 11:19:43 2023 +0200
@@ -93,7 +93,7 @@
case _ => false
}
- def interruptible_capture[A](e: => A): Result[A] =
+ def result[A](e: => A): Result[A] =
try { Res(e) }
catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
--- a/src/Pure/General/file_stream.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/file_stream.ML Fri Sep 29 11:19:43 2023 +0200
@@ -27,11 +27,12 @@
val platform_path = ML_System.platform_path o Path.implode o Path.expand;
fun with_file open_file close_file f =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+ Thread_Attributes.uninterruptible (fn run => fn path =>
let
val file = open_file path;
- val result = Exn.capture (restore_attributes f) file;
- in close_file file; Exn.release result end);
+ val result = Exn.capture (run f) file;
+ val _ = close_file file;
+ in Exn.release result end);
in
--- a/src/Pure/General/same.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/same.ML Fri Sep 29 11:19:43 2023 +0200
@@ -13,7 +13,6 @@
val same: ('a, 'b) function
val commit: 'a operation -> 'a -> 'a
val function: ('a -> 'b option) -> ('a, 'b) function
- val capture: ('a, 'b) function -> 'a -> 'b option
val map: 'a operation -> 'a list operation
val map_option: ('a, 'b) function -> ('a option, 'b option) function
end;
@@ -29,8 +28,6 @@
fun same _ = raise SAME;
fun commit f x = f x handle SAME => x;
-fun capture f x = SOME (f x) handle SAME => NONE;
-
fun function f x =
(case f x of
NONE => raise SAME
--- a/src/Pure/General/sha1.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/sha1.ML Fri Sep 29 11:19:43 2023 +0200
@@ -155,12 +155,12 @@
(Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
fun with_memory n =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
+ Thread_Attributes.uninterruptible (fn run => fn f =>
let
val mem = Foreign.Memory.malloc (Word.fromInt n);
- val res = Exn.capture (restore_attributes f) mem;
+ val result = Exn.capture (run f) mem;
val _ = Foreign.Memory.free mem;
- in Exn.release res end);
+ in Exn.release result end);
(* digesting *)
--- a/src/Pure/General/socket_io.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/socket_io.ML Fri Sep 29 11:19:43 2023 +0200
@@ -88,11 +88,13 @@
handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ socket_name);
fun with_streams f =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn socket_name =>
+ Thread_Attributes.uninterruptible (fn run => fn socket_name =>
let
val streams = open_streams socket_name;
- val result = Exn.capture (restore_attributes f) streams;
- in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
+ val result = Exn.capture (run f) streams;
+ val _ = BinIO.closeIn (#1 streams);
+ val _ = BinIO.closeOut (#2 streams);
+ in Exn.release result end);
fun with_streams' f socket_name password =
with_streams (fn streams =>
--- a/src/Pure/General/timing.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/timing.ML Fri Sep 29 11:19:43 2023 +0200
@@ -90,7 +90,7 @@
fun cond_timeit enabled msg e =
if enabled then
let
- val (t, result) = timing (Exn.interruptible_capture e) ();
+ val (t, result) = timing (Exn.result e) ();
val _ =
if is_relevant t then
let val end_msg = message t
@@ -111,7 +111,7 @@
fun protocol name pos f x =
let
- val (t, result) = timing (Exn.interruptible_capture f) x;
+ val (t, result) = timing (Exn.result f) x;
val _ = protocol_message name pos t;
in Exn.release result end;
--- a/src/Pure/Isar/attrib.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Sep 29 11:19:43 2023 +0200
@@ -613,6 +613,7 @@
register_config_string ML_Env.ML_environment #>
register_config_bool ML_Env.ML_read_global #>
register_config_bool ML_Env.ML_write_global #>
+ register_config_bool ML_Compiler.ML_catch_all #>
register_config_bool ML_Options.source_trace #>
register_config_bool ML_Options.exception_trace #>
register_config_bool ML_Options.exception_debugger #>
--- a/src/Pure/Isar/proof.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Isar/proof.ML Fri Sep 29 11:19:43 2023 +0200
@@ -1259,7 +1259,7 @@
val test_proof =
local_skip_proof true
|> Unsynchronized.setmp testing true
- |> Exn.interruptible_capture;
+ |> Exn.result;
fun after_qed' (result_ctxt, results) state' = state'
|> refine_goals print_rule result_ctxt (flat results)
--- a/src/Pure/Isar/toplevel.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Sep 29 11:19:43 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/ML/exn_debugger.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/exn_debugger.ML Fri Sep 29 11:19:43 2023 +0200
@@ -42,10 +42,10 @@
in
fun capture_exception_trace e =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val _ = start_trace ();
- val result = Exn.interruptible_capture (restore_attributes e) ();
+ val result = Exn.result (run e) ();
val trace = stop_trace ();
val trace' =
(case result of
@@ -54,7 +54,7 @@
trace
|> map_filter (fn (entry, e) => if eq_exn (exn, e) then SOME entry else NONE)
|> rev);
- in (trace', result) end) ();
+ in (trace', result) end);
end;
--- a/src/Pure/ML/exn_properties.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/exn_properties.ML Fri Sep 29 11:19:43 2023 +0200
@@ -63,8 +63,8 @@
startLine = #startLine loc, endLine = #endLine loc,
startPosition = #startPosition loc, endPosition = #endPosition loc};
in
- Thread_Attributes.uninterruptible (fn _ => fn () =>
- PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
+ Thread_Attributes.uninterruptible_body (fn _ =>
+ PolyML.raiseWithLocation (exn, loc') handle exn' => exn')
end
end;
--- a/src/Pure/ML/ml_antiquotation.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Fri Sep 29 11:19:43 2023 +0200
@@ -18,7 +18,9 @@
val inline_embedded: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
val value_embedded: binding -> string context_parser -> theory -> theory
- val special_form: binding -> string -> theory -> theory
+ val special_form: binding ->
+ (Proof.context -> Input.source -> string * ML_Lex.token Antiquote.antiquote list list) ->
+ theory -> theory
val conditional: binding -> (Proof.context -> bool) -> theory -> theory
end;
@@ -67,23 +69,31 @@
(* ML macros *)
-fun special_form binding operator =
+fun special_form binding parse =
ML_Context.add_antiquotation binding true
(fn _ => fn src => fn ctxt =>
let
- val s = Token.read ctxt Parse.embedded_input src;
+ val input = Token.read ctxt Parse.embedded_input src;
val tokenize = ML_Lex.tokenize_no_range;
- val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
+ val tokenize_range = ML_Lex.tokenize_range (Input.range_of input);
+ val eq = tokenize " = ";
- val (decl, ctxt') = ML_Context.read_antiquotes s ctxt;
+ val (operator, sections) = parse ctxt input;
+ val (decls, ctxt') = ML_Context.expand_antiquotes_list sections ctxt;
fun decl' ctxt'' =
let
- val (ml_env, ml_body) = decl ctxt'';
+ val (sections_env, sections_body) = split_list (decls ctxt'');
+ val sections_bind =
+ sections_body |> map_index (fn (i, body) =>
+ let
+ val name = tokenize ("expr" ^ (if i = 0 then "" else string_of_int i));
+ val bind = if i = 0 then tokenize "val " else tokenize "and ";
+ in (bind @ name @ eq @ body, name) end);
val ml_body' =
- tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @
- tokenize " val " @ tokenize_range "result" @
- tokenize (" = " ^ operator ^ " expr; in result end");
- in (ml_env, ml_body') end;
+ tokenize "let " @ maps #1 sections_bind @
+ tokenize " val " @ tokenize_range "result" @ eq @
+ tokenize operator @ maps #2 sections_bind @ tokenize " in result end";
+ in (flat sections_env, ml_body') end;
in (decl', ctxt') end);
fun conditional binding check =
--- a/src/Pure/ML/ml_antiquotations.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Fri Sep 29 11:19:43 2023 +0200
@@ -340,12 +340,67 @@
in end;
-(* special forms for option type *)
+(* exception handling *)
+
+local
+
+val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range;
+val tokenize_range_text = map Antiquote.Text oo ML_Lex.tokenize_range;
+
+val bg_expr = tokenize_text "(fn () =>";
+val en_expr = tokenize_text ")";
+fun make_expr a = bg_expr @ a @ en_expr;
+
+fun make_handler range a =
+ tokenize_range_text range "(fn" @ a @
+ tokenize_range_text range "| exn => Exn.reraise exn)";
+
+fun report_special tok = (ML_Lex.pos_of tok, Markup.keyword3);
+
+fun print_special tok =
+ let val (pos, markup) = report_special tok
+ in Markup.markup markup (ML_Lex.content_of tok) ^ Position.here pos end;
+
+val is_catch = ML_Lex.is_ident_with (fn x => x = "catch");
+val is_finally = ML_Lex.is_ident_with (fn x => x = "finally");
+fun is_special t = is_catch t orelse is_finally t;
+val is_special_text = fn Antiquote.Text t => is_special t | _ => false;
+
+fun parse_try ctxt input =
+ let
+ val ants = ML_Lex.read_source input;
+ val specials = ants
+ |> map_filter (fn Antiquote.Text t => if is_special t then SOME t else NONE | _ => NONE);
+ val _ = Context_Position.reports ctxt (map report_special specials);
+ in
+ (case specials of
+ [] => ("Isabelle_Thread.try", [make_expr ants])
+ | [s] =>
+ let val (a, b) = ants |> chop_prefix (not o is_special_text) ||> tl in
+ if is_finally s
+ then ("Isabelle_Thread.try_finally", [make_expr a, make_expr b])
+ else ("Isabelle_Thread.try_catch", [make_expr a, make_handler (ML_Lex.range_of s) b])
+ end
+ | _ => error ("Too many special keywords: " ^ commas (map print_special specials)))
+ end;
+
+fun parse_can (_: Proof.context) input =
+ ("Isabelle_Thread.can", [make_expr (ML_Lex.read_source input)]);
+
+in
val _ = Theory.setup
- (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "Isabelle_Thread.try" #>
- ML_Antiquotation.special_form \<^binding>\<open>can\<close> "Isabelle_Thread.can" #>
- ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
+ (ML_Antiquotation.special_form \<^binding>\<open>try\<close> parse_try #>
+ ML_Antiquotation.special_form \<^binding>\<open>can\<close> parse_can);
+
+end;
+
+
+
+(* special form for option type *)
+
+val _ = Theory.setup
+ (ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
(fn _ => fn src => fn ctxt =>
let
val s = Token.read ctxt Parse.embedded_input src;
--- a/src/Pure/ML/ml_compiler.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_compiler.ML Fri Sep 29 11:19:43 2023 +0200
@@ -7,11 +7,12 @@
signature ML_COMPILER =
sig
type flags =
- {environment: string, redirect: bool, verbose: bool,
+ {environment: string, redirect: bool, verbose: bool, catch_all: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit}
val debug_flags: bool option -> flags
val flags: flags
val verbose: bool -> flags -> flags
+ val ML_catch_all: bool Config.T
val eval: flags -> Position.T -> ML_Lex.token list -> unit
end;
@@ -21,18 +22,18 @@
(* flags *)
type flags =
- {environment: string, redirect: bool, verbose: bool,
+ {environment: string, redirect: bool, verbose: bool, catch_all: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit};
fun debug_flags opt_debug : flags =
- {environment = "", redirect = false, verbose = false,
+ {environment = "", redirect = false, verbose = false, catch_all = false,
debug = opt_debug, writeln = writeln, warning = warning};
val flags = debug_flags NONE;
-fun verbose b (flags: flags) =
- {environment = #environment flags, redirect = #redirect flags, verbose = b,
- debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+fun verbose b ({environment, redirect, verbose = _, catch_all, debug, writeln, warning}: flags) =
+ {environment = environment, redirect = redirect, verbose = b, catch_all = catch_all,
+ debug = debug, writeln = writeln, warning = warning};
(* parse trees *)
@@ -147,6 +148,8 @@
(* eval ML source tokens *)
+val ML_catch_all = Config.declare_bool ("ML_catch_all", \<^here>) (K false);
+
fun eval (flags: flags) pos toks =
let
val opt_context = Context.get_generic_context ();
@@ -201,16 +204,29 @@
val error_buffer = Unsynchronized.ref Buffer.empty;
fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
- fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
- fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
+
+ fun expose_error verbose =
+ let
+ val msg = Buffer.content (! error_buffer);
+ val is_err = msg <> "";
+ val _ = if is_err orelse verbose then (output_warnings (); output_writeln ()) else ();
+ in if is_err then error (trim_line msg) else () end;
fun message {message = msg, hard, location = loc, context = _} =
let
val pos = Exn_Properties.position_of_polyml_location loc;
- val txt =
- (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
- Pretty.string_of (Pretty.from_polyml msg);
- in if hard then err txt else warn txt end;
+ val s = Pretty.string_of (Pretty.from_polyml msg);
+ val catch_all =
+ #catch_all flags orelse
+ (case opt_context of
+ NONE => false
+ | SOME context => Config.get_generic context ML_catch_all);
+ val is_err =
+ hard orelse
+ (not catch_all andalso
+ String.isPrefix "Handler catches all exceptions" (XML.content_of (YXML.parse_body s)));
+ val txt = (if is_err then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ s;
+ in if is_err then err txt else warn txt end;
(* results *)
@@ -294,12 +310,8 @@
STATIC_ERRORS () => ""
| Runtime.TOPLEVEL_ERROR => ""
| _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
- val _ = output_warnings ();
- val _ = output_writeln ();
- in raise_error exn_msg end;
- in
- if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
- else ()
- end;
+ val _ = err exn_msg;
+ in expose_error true end;
+ in expose_error (#verbose flags) end;
end;
--- a/src/Pure/ML/ml_compiler0.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_compiler0.ML Fri Sep 29 11:19:43 2023 +0200
@@ -117,11 +117,12 @@
end;
-fun ML_file context {verbose, debug} file =
+fun ML_file context {verbose, debug} file = Thread_Attributes.uninterruptible_body (fn run =>
let
val instream = TextIO.openIn file;
- val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in ML context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+ val result = Exn.capture (run TextIO.inputAll) instream;
+ val _ = TextIO.closeIn instream;
+ in ML context {line = 1, file = file, verbose = verbose, debug = debug} (Exn.release result) end);
fun ML_file_operations (f: bool option -> string -> unit) =
{ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)};
--- a/src/Pure/ML/ml_context.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_context.ML Fri Sep 29 11:19:43 2023 +0200
@@ -238,3 +238,4 @@
end;
val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);
+val ML_command = ML_Context.eval_source ML_Compiler.flags;
--- a/src/Pure/ML/ml_file.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_file.ML Fri Sep 29 11:19:43 2023 +0200
@@ -6,7 +6,7 @@
signature ML_FILE =
sig
- val command: string -> bool option -> (theory -> Token.file) ->
+ val command: string -> bool -> bool option -> (theory -> Token.file) ->
Toplevel.transition -> Toplevel.transition
val ML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
val SML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
@@ -15,7 +15,7 @@
structure ML_File: ML_FILE =
struct
-fun command environment debug get_file = Toplevel.generic_theory (fn gthy =>
+fun command environment catch_all debug get_file = Toplevel.generic_theory (fn gthy =>
let
val file = get_file (Context.theory_of gthy);
val provide = Resources.provide_file file;
@@ -24,7 +24,7 @@
val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
val flags: ML_Compiler.flags =
- {environment = environment, redirect = true, verbose = true,
+ {environment = environment, redirect = true, verbose = true, catch_all = catch_all,
debug = debug, writeln = writeln, warning = warning};
in
gthy
@@ -34,7 +34,7 @@
|> Context.mapping provide (Local_Theory.background_theory provide)
end);
-val ML = command "";
-val SML = command ML_Env.SML;
+val ML = command "" false;
+val SML = command ML_Env.SML true;
end;
--- a/src/Pure/ML/ml_lex.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_lex.ML Fri Sep 29 11:19:43 2023 +0200
@@ -12,6 +12,7 @@
Space | Comment of Comment.kind option | Error of string | EOF
eqtype token
val stopper: token Scan.stopper
+ val is_ident_with: (string -> bool) -> token -> bool
val is_regular: token -> bool
val is_improper: token -> bool
val is_comment: token -> bool
@@ -110,6 +111,9 @@
fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x)
| is_delimiter _ = false;
+fun is_ident_with pred (Token (_, (Ident, x))) = pred x
+ | is_ident_with _ _ = false;
+
fun is_regular (Token (_, (Error _, _))) = false
| is_regular (Token (_, (EOF, _))) = false
| is_regular _ = true;
--- a/src/Pure/ML_Bootstrap.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML_Bootstrap.thy Fri Sep 29 11:19:43 2023 +0200
@@ -35,6 +35,6 @@
setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
-declare [[ML_read_global = false]]
+declare [[ML_read_global = false, ML_catch_all = true]]
end
--- a/src/Pure/PIDE/command.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/command.ML Fri Sep 29 11:19:43 2023 +0200
@@ -81,7 +81,7 @@
let val _ = Position.report pos (Markup.language_path delimited) in
case content of
NONE =>
- Exn.interruptible_capture (fn () =>
+ Exn.result (fn () =>
Resources.read_file_node file_node master_dir (src_path, pos)) ()
| SOME (digest, lines) => Exn.Res (blob_file src_path lines digest file_node)
end
@@ -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) ();
@@ -222,7 +224,7 @@
fun eval_state keywords span tr ({state, ...}: eval_state) =
let
- val _ = Thread_Attributes.expose_interrupt ();
+ val _ = Isabelle_Thread.expose_interrupt ();
val st = reset_state keywords tr state;
@@ -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 Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/document.ML Fri Sep 29 11:19:43 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' =
@@ -783,10 +786,10 @@
Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
let
val _ = Output.status [Markup.markup_only Markup.consolidating];
- val res = Exn.capture (Thy_Info.apply_presentation context) thy;
+ val result = Exn.capture (Thy_Info.apply_presentation context) thy;
val _ = Lazy.force (get_consolidated node);
val _ = Output.status [Markup.markup_only Markup.consolidated];
- in Exn.release res end};
+ in Exn.release result end};
val result_entry =
(case lookup_entry node id of
NONE => err_undef "result command entry" id
--- a/src/Pure/PIDE/protocol.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/protocol.ML Fri Sep 29 11:19:43 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 Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/protocol_command.ML Fri Sep 29 11:19:43 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/PIDE/query_operation.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/query_operation.ML Fri Sep 29 11:19:43 2023 +0200
@@ -19,7 +19,7 @@
Command.print_function (name ^ "_query")
(fn {args = instance :: args, ...} =>
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
- print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state =>
+ print_fn = fn _ => Thread_Attributes.uninterruptible (fn run => fn state =>
let
fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
fun status m = output_result (Markup.markup_only m);
@@ -28,11 +28,11 @@
output_result (Markup.markup Markup.error (Runtime.exn_message exn));
val _ = status Markup.running;
- fun run () =
+ fun main () =
f {state = state, args = args, output_result = output_result,
writeln_result = writeln_result};
val _ =
- (case Exn.capture (*sic!*) (restore_attributes run) () of
+ (case Exn.capture (*sic!*) (run main) () of
Exn.Res () => ()
| Exn.Exn exn => toplevel_error exn);
val _ = status Markup.finished;
--- a/src/Pure/Pure.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Pure.thy Fri Sep 29 11:19:43 2023 +0200
@@ -246,7 +246,7 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {environment = ML_Env.SML_export, redirect = false, verbose = true,
+ {environment = ML_Env.SML_export, redirect = false, verbose = true, catch_all = true,
debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.theory
@@ -258,7 +258,7 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {environment = ML_Env.SML_import, redirect = false, verbose = true,
+ {environment = ML_Env.SML_import, redirect = false, verbose = true, catch_all = true,
debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.generic_theory
@@ -1558,4 +1558,6 @@
declare [[ML_write_global = false]]
+ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>
+
end
--- a/src/Pure/ROOT.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ROOT.ML Fri Sep 29 11:19:43 2023 +0200
@@ -28,6 +28,8 @@
ML_file "Concurrent/unsynchronized.ML";
ML_file "Concurrent/synchronized.ML";
ML_file "Concurrent/counter.ML";
+ML_file "Concurrent/single_assignment.ML";
+ML_file "Concurrent/isabelle_thread.ML";
ML_file "ML/ml_heap.ML";
ML_file "ML/ml_print_depth0.ML";
@@ -121,8 +123,6 @@
ML_file_no_debug "ML/exn_debugger.ML";
ML_file "Concurrent/thread_data_virtual.ML";
-ML_file "Concurrent/single_assignment.ML";
-ML_file "Concurrent/isabelle_thread.ML";
ML_file "Concurrent/par_exn.ML";
ML_file "Concurrent/task_queue.ML";
--- a/src/Pure/Syntax/syntax_phases.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Sep 29 11:19:43 2023 +0200
@@ -215,7 +215,7 @@
[ast] => ast
| asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
- val ast = Exn.interruptible_capture ast_of parsetree;
+ val ast = Exn.result ast_of parsetree;
in (! reports, ast) end;
@@ -310,7 +310,7 @@
SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t)
| NONE => t);
- val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+ val tm' = Exn.result (fn () => decode [] [] [] tm) ();
in (! reports, tm') end;
end;
@@ -370,7 +370,7 @@
val (ambig_msgs, asts) = parse_asts ctxt false root input;
val results =
(map o apsnd o Exn.maps_res)
- (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
+ (Ast.normalize ctxt parse_rules #> Exn.result (ast_to_term ctxt tr)) asts;
in (ambig_msgs, results) end;
--- a/src/Pure/System/command_line.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/command_line.ML Fri Sep 29 11:19:43 2023 +0200
@@ -13,11 +13,16 @@
struct
fun tool body =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
+ fun print_failure exn = (Runtime.exn_error_message exn; Exn.failure_rc exn);
val rc =
- (restore_attributes body (); 0) handle exn =>
- ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
- in exit rc end) ();
+ (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 Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/isabelle_process.ML Fri Sep 29 11:19:43 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 () =
@@ -197,6 +203,7 @@
Multithreading.trace := Options.default_int "threads_trace";
Multithreading.max_threads_update (Options.default_int "threads");
Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
+ Isabelle_Thread.threads_stack_limit := Options.default_real "threads_stack_limit";
if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
let val proofs = Options.default_int "record_proofs"
in if proofs < 0 then () else Proofterm.proofs := proofs end;
--- a/src/Pure/System/isabelle_system.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/isabelle_system.ML Fri Sep 29 11:19:43 2023 +0200
@@ -40,7 +40,7 @@
let
val {script, input, cwd, putenv, redirect, timeout, description} =
Bash.dest_params params;
- val run =
+ val server_run =
[Bash.server_run, script, input,
let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
let open XML.Encode in YXML.string_of_body o list (pair string string) end
@@ -59,11 +59,11 @@
with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid])
| kill NONE = ();
in
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
fun err () = raise Fail "Malformed result from bash_process server";
- fun loop maybe_uuid s =
- (case restore_attributes Byte_Message.read_message_string (#1 s) of
+ 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
loop (SOME (hd args)) s
@@ -88,8 +88,13 @@
end
else err ()
| _ => err ())
- handle exn => (kill maybe_uuid; Exn.reraise exn);
- in with_streams (fn s => (Byte_Message.write_message_string (#2 s) run; loop NONE s)) end) ()
+ 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)
end;
val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc;
@@ -138,18 +143,25 @@
raise Fail ("Temporary file already exists: " ^ Path.print path);
in path end;
-fun with_tmp_file name ext f =
- let val path = create_tmp_path name ext
- in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
+fun with_tmp_file name ext = Thread_Attributes.uninterruptible (fn run => fn f =>
+ let
+ val path = create_tmp_path name ext;
+ val result = Exn.capture (run f) path;
+ val _ = try File.rm path;
+ in Exn.release result end);
(* tmp dirs *)
fun rm_tree path = scala_function "rm_tree" [path];
-fun with_tmp_dir name f =
- let val path = create_tmp_path name ""
- in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
+fun with_tmp_dir name = Thread_Attributes.uninterruptible (fn run => fn f =>
+ let
+ val path = create_tmp_path name "";
+ val _ = make_directory path;
+ val result = Exn.capture (run f) path;
+ val _ = try rm_tree path;
+ in Exn.release result end);
(* download file *)
--- a/src/Pure/System/scala.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/scala.ML Fri Sep 29 11:19:43 2023 +0200
@@ -42,7 +42,7 @@
in
fun function_bytes name args =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val id = new_id ();
fun invoke () =
@@ -60,9 +60,10 @@
| NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
in
invoke ();
- Exn.release (restore_attributes await_result ())
- handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
- end) ();
+ (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/Thy/thy_info.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Sep 29 11:19:43 2023 +0200
@@ -216,9 +216,9 @@
| consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
let
val _ = Execution.join [exec_id];
- val res = Exn.capture Thm.consolidate_theory theory;
+ val result = Exn.capture Thm.consolidate_theory theory;
val exns = maps Task_Queue.group_status (Execution.peek exec_id);
- in res :: map Exn.Exn exns end;
+ in result :: map Exn.Exn exns end;
fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
| present_theory (Exn.Res (Result {theory, present, ...})) =
--- a/src/Pure/Tools/build.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/build.ML Fri Sep 29 11:19:43 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/build.scala Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/build.scala Fri Sep 29 11:19:43 2023 +0200
@@ -856,7 +856,7 @@
val errors = new mutable.ListBuffer[String]
for (session_name <- sessions) {
- Exn.interruptible_capture(print(session_name)) match {
+ Exn.result(print(session_name)) match {
case Exn.Res(_) =>
case Exn.Exn(exn) => errors += Exn.message(exn)
}
--- a/src/Pure/Tools/debugger.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/debugger.ML Fri Sep 29 11:19:43 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 *)
@@ -137,7 +137,7 @@
fun evaluate {SML, verbose} =
ML_Context.eval
- {environment = environment SML, redirect = false, verbose = verbose,
+ {environment = environment SML, redirect = false, verbose = verbose, catch_all = SML,
debug = SOME false, writeln = writeln_message, warning = warning_message}
Position.none;
@@ -229,13 +229,13 @@
in
fun debugger_loop thread_name =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
fun loop () =
(debugger_state thread_name; if debugger_command thread_name then loop () else ());
- val result = Exn.capture (restore_attributes with_debugging) loop;
+ val result = Exn.capture (run with_debugging) loop;
val _ = debugger_state thread_name;
- in Exn.release result end) ();
+ in Exn.release result end);
end;
--- a/src/Pure/Tools/simplifier_trace.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Fri Sep 29 11:19:43 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;
--- a/src/Tools/Code/code_runtime.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Tools/Code/code_runtime.ML Fri Sep 29 11:19:43 2023 +0200
@@ -99,7 +99,7 @@
val (program_code, value_name) = comp vs_t;
val value_code = space_implode " "
(value_name :: "()" :: map (enclose "(" ")") args);
- in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
+ in Exn.result (value ctxt cookie) (program_code, value_code) end;
fun partiality_as_none e = SOME (Exn.release e)
handle General.Match => NONE
@@ -390,7 +390,7 @@
fun checked_computation cTs raw_computation ctxt =
check_computation_input ctxt cTs
- #> Exn.interruptible_capture raw_computation
+ #> Exn.result raw_computation
#> partiality_as_none;
fun mount_computation ctxt cTs T raw_computation lift_postproc =
--- a/src/Tools/quickcheck.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Tools/quickcheck.ML Fri Sep 29 11:19:43 2023 +0200
@@ -262,7 +262,7 @@
try tester v
else
let (* FIXME !?!? *)
- val tester = Exn.interruptible_capture tester v
+ val tester = Exn.result tester v
in
(case Exn.get_res tester of
NONE => SOME (Exn.release tester)
--- a/src/Tools/try.ML Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Tools/try.ML Fri Sep 29 11:19:43 2023 +0200
@@ -83,17 +83,18 @@
persistent = true,
strict = true,
print_fn = fn _ => fn st =>
- let
- val state = Toplevel.proof_of st
- |> Proof.map_context (Context_Position.set_visible false)
- val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
- in
- if auto_time_limit > 0.0 then
- (case Timeout.apply_physical (seconds auto_time_limit) (fn () => body true state) () of
- (true, (_, outcome)) => List.app Output.information outcome
- | _ => ())
- else ()
- end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
+ \<^try>\<open>
+ let
+ val state = Toplevel.proof_of st
+ |> Proof.map_context (Context_Position.set_visible false)
+ val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
+ in
+ if auto_time_limit > 0.0 then
+ (case Timeout.apply_physical (seconds auto_time_limit) (fn () => body true state) () of
+ (true, (_, outcome)) => List.app Output.information outcome
+ | _ => ())
+ else ()
+ end catch _ => ()\<close>}
else NONE);