# HG changeset patch
# User wenzelm
# Date 1614028001 -3600
# Node ID 0e7a3c055f39ae8754fc5e2966888634f2b124a1
# Parent  a97ae083cad120b683f350691895857412936466
clarified uses of Isabelle_System.bash_process: more checks, fewer messages;

diff -r a97ae083cad1 -r 0e7a3c055f39 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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
 
 
diff -r a97ae083cad1 -r 0e7a3c055f39 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Feb 22 18:19:38 2021 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Feb 22 22:06:41 2021 +0100
@@ -263,11 +263,11 @@
           " -o " ^ File.bash_platform_path executable ^ ";"
         val compilation_time =
           Isabelle_System.bash_process cmd
-          |> Process_Result.print
-          |> Process_Result.timing_elapsed |> Time.toMilliseconds;
+          |> Process_Result.check
+          |> Process_Result.timing_elapsed |> Time.toMilliseconds
+          handle ERROR msg => cat_error "Compilation with GHC failed" msg
         val _ = Quickcheck.add_timing ("Haskell compilation", compilation_time) current_result
         fun haskell_string_of_bool v = if v then "True" else "False"
-        val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
         fun with_size genuine_only k =
           if k > size then (NONE, !current_result)
           else
@@ -277,9 +277,9 @@
               val res =
                 Isabelle_System.bash_process
                   (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
-                    string_of_int k);
-              val _ = warning (Process_Result.err res);
-              val response = Process_Result.out res;
+                    string_of_int k)
+                |> Process_Result.check
+              val response = Process_Result.out res
               val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds;
               val _ =
                 Quickcheck.add_timing