# HG changeset patch
# User haftmann
# Date 1360759132 -3600
# Node ID c007c6bf4a35ed39b2e878cc570f839a468459e2
# Parent  bee2678a3b61129481d5c734413b6eb633c4cb11
another attempt for a uniform abort on code generation errors

diff -r bee2678a3b61 -r c007c6bf4a35 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/Tools/Code/code_ml.ML	Wed Feb 13 13:38:52 2013 +0100
@@ -833,7 +833,7 @@
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn _ =>
-          "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' Pure" } })
+          "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   #> Code_Target.add_target
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",
diff -r bee2678a3b61 -r c007c6bf4a35 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/Tools/Code/lib/Tools/codegen	Wed Feb 13 13:38:52 2013 +0100
@@ -52,7 +52,7 @@
 
 FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
   (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
-  handle _ => Posix.Process.exit 0w1;"
+  handle _ => exit 1;"
 
 ACTUAL_CMD="val thyname = \"$THYNAME\"; \
   val _ = quick_and_dirty := $QUICK_AND_DIRTY; \