src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 73285 0e7a3c055f39
parent 73277 0110e2e2964c
child 74142 0f051404f487
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 22 18:19:38 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 22 22:06:41 2021 +0100
@@ -818,11 +818,12 @@
     if getenv env_var = "" then
       (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
     else
-      (case Isabelle_System.bash_output (cmd ^ File.bash_path file) of
-        (out, 0) => out
-      | (_, rc) =>
-          error ("Error caused by prolog system " ^ env_var ^
-            ": return code " ^ string_of_int rc))
+      let val res = Isabelle_System.bash_process (cmd ^ File.bash_path file) in
+        res |> Process_Result.check |> Process_Result.out
+          handle ERROR msg =>
+            cat_error ("Error caused by prolog system " ^ env_var ^
+              ": return code " ^ string_of_int (Process_Result.rc res)) msg
+      end
   end