--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Sep 25 20:56:44 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/Tools/Mirabelle/mirabelle.ML Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Sep 25 20:56:44 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/Sledgehammer/sledgehammer.ML Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 25 20:56:44 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 Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Sep 25 20:56:44 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_smt.ML Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Sep 25 20:56:44 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/Tools/try.ML Mon Sep 25 19:49:25 2023 +0200
+++ b/src/Tools/try.ML Mon Sep 25 20:56:44 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);