# HG changeset patch
# User wenzelm
# Date 1695922614 -7200
# Node ID 810eca7539197ab79fd5ba10bfafb9030370509d
# Parent  3c02ad5a15864f96b525f4192a4a6f0671e3f7a6
tuned: prefer try-catch/finally over low-level 'handle';

diff -r 3c02ad5a1586 -r 810eca753919 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Sep 28 14:43:07 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Sep 28 19:36:54 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
 
diff -r 3c02ad5a1586 -r 810eca753919 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Sep 28 14:43:07 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Sep 28 19:36:54 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))))