# HG changeset patch
# User wenzelm
# Date 1365782211 -7200
# Node ID 0b0fc7dc4ce4f77bb9d8e669b47d64f740d754b4
# Parent  f2e92fc0c8aaabe50b74d850a44b28ca911782c0
actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;

diff -r f2e92fc0c8aa -r 0b0fc7dc4ce4 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Apr 12 17:21:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Apr 12 17:56:51 2013 +0200
@@ -791,7 +791,12 @@
   in
     if getenv env_var = "" then
       (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
-    else fst (Isabelle_System.bash_output (cmd ^ File.shell_path file))
+    else
+      (case Isabelle_System.bash_output (cmd ^ File.shell_path file) of
+        (out, 0) => out
+      | (_, rc) =>
+          error ("Error caused by prolog system " ^ env_var ^
+            ": return code " ^ string_of_int rc))
   end