# HG changeset patch
# User wenzelm
# Date 1344002412 -7200
# Node ID b171bcd5dd86579a000354ae3544daf371ad61bf
# Parent  9149ebdd02410710811ea6b7d08ae543ff4be9e6
more informative process exit code;

diff -r 9149ebdd0241 -r b171bcd5dd86 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Fri Aug 03 14:52:45 2012 +0200
+++ b/lib/scripts/run-polyml	Fri Aug 03 16:00:12 2012 +0200
@@ -46,10 +46,10 @@
 
 if [ -z "$INFILE" ]; then
   INIT=""
-  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.failure));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
   EXIT=""
 fi
 
diff -r 9149ebdd0241 -r b171bcd5dd86 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Fri Aug 03 14:52:45 2012 +0200
+++ b/lib/scripts/run-smlnj	Fri Aug 03 16:00:12 2012 +0200
@@ -52,7 +52,7 @@
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
-  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
   DB=""
 else
   EXIT=""
diff -r 9149ebdd0241 -r b171bcd5dd86 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Fri Aug 03 14:52:45 2012 +0200
+++ b/src/Pure/System/build.ML	Fri Aug 03 16:00:12 2012 +0200
@@ -79,7 +79,9 @@
     val _ = Session.finish ();
     val _ = if do_output then () else quit ();
   in () end
-  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
+  handle exn =>
+    (Output.error_msg (ML_Compiler.exn_message exn);
+     if Exn.is_interrupt exn then exit 130 else exit 1);
 
 end;
 
diff -r 9149ebdd0241 -r b171bcd5dd86 src/Pure/build
--- a/src/Pure/build	Fri Aug 03 14:52:45 2012 +0200
+++ b/src/Pure/build	Fri Aug 03 16:00:12 2012 +0200
@@ -61,11 +61,11 @@
 if [ "$TARGET" = RAW ]; then
   if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
-      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
+      -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \
       -q RAW_ML_SYSTEM
   else
     "$ISABELLE_PROCESS" \
-      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
+      -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \
       -e "structure Isar = struct fun main () = () end;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -q -w RAW_ML_SYSTEM "$OUTPUT"
@@ -73,11 +73,11 @@
 else
   if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
-      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
       -q RAW_ML_SYSTEM
   else
     "$ISABELLE_PROCESS" \
-      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -f -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
diff -r 9149ebdd0241 -r b171bcd5dd86 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Fri Aug 03 14:52:45 2012 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Fri Aug 03 16:00:12 2012 +0200
@@ -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 _ => OS.Process.exit OS.Process.failure;"
+  handle _ => Posix.Process.exit 0w1;"
 
 ACTUAL_CMD="val thyname = \"$THYNAME\"; \
   val _ = quick_and_dirty := $QUICK_AND_DIRTY; \