# HG changeset patch
# User wenzelm
# Date 1695668965 -7200
# Node ID 27b2368ca69d01302214080934c8e02d409f7bbe
# Parent  ebafb2daabb771a1c572870f298bd55f29b85347
tuned: prefer antiquotation for try-catch;

diff -r ebafb2daabb7 -r 27b2368ca69d src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Mon Sep 25 20:56:44 2023 +0200
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Mon Sep 25 21:09:25 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 =