# HG changeset patch
# User wenzelm
# Date 1695668204 -7200
# Node ID ebafb2daabb771a1c572870f298bd55f29b85347
# Parent  72d2693fb0ecd61add4d1f16af9a0c87d67926a8
tuned: prefer antiquotation for try-catch;

diff -r 72d2693fb0ec -r ebafb2daabb7 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- 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
diff -r 72d2693fb0ec -r ebafb2daabb7 src/HOL/Tools/Mirabelle/mirabelle.ML
--- 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);
diff -r 72d2693fb0ec -r ebafb2daabb7 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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
diff -r 72d2693fb0ec -r ebafb2daabb7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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), " ^
diff -r 72d2693fb0ec -r ebafb2daabb7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- 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
diff -r 72d2693fb0ec -r ebafb2daabb7 src/Tools/try.ML
--- 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);