# HG changeset patch
# User wenzelm
# Date 1398160077 -7200
# Node ID cb912b7de3cfda02befe662749e7995818588612
# Parent  6532efd66a70a6f4e05efe401f34cb07867d5b0e
more general exit;

diff -r 6532efd66a70 -r cb912b7de3cf lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Apr 21 21:16:05 2014 +0200
+++ b/lib/scripts/run-polyml	Tue Apr 22 11:47:57 2014 +0200
@@ -41,7 +41,7 @@
 
 if [ -z "$INFILE" ]; then
   INIT=""
-  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
+  EXIT="fun exit rc = 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 exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
diff -r 6532efd66a70 -r cb912b7de3cf lib/scripts/run-polyml-5.5.1
--- a/lib/scripts/run-polyml-5.5.1	Mon Apr 21 21:16:05 2014 +0200
+++ b/lib/scripts/run-polyml-5.5.1	Tue Apr 22 11:47:57 2014 +0200
@@ -42,7 +42,7 @@
 
 if [ -z "$INFILE" ]; then
   INIT=""
-  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
+  EXIT="fun exit rc = 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 exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
diff -r 6532efd66a70 -r cb912b7de3cf lib/scripts/run-polyml-5.5.2
--- a/lib/scripts/run-polyml-5.5.2	Mon Apr 21 21:16:05 2014 +0200
+++ b/lib/scripts/run-polyml-5.5.2	Tue Apr 22 11:47:57 2014 +0200
@@ -42,7 +42,7 @@
 
 if [ -z "$INFILE" ]; then
   INIT=""
-  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
+  EXIT="fun exit rc = 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 exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
diff -r 6532efd66a70 -r cb912b7de3cf lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Apr 21 21:16:05 2014 +0200
+++ b/lib/scripts/run-smlnj	Tue Apr 22 11:47:57 2014 +0200
@@ -54,7 +54,7 @@
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
-  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
+  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
   DB=""
 else
   EXIT=""
diff -r 6532efd66a70 -r cb912b7de3cf src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Apr 21 21:16:05 2014 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Apr 22 11:47:57 2014 +0200
@@ -9,6 +9,9 @@
 exception Interrupt;
 fun reraise exn = raise exn;
 
+fun exit rc = Posix.Process.exit (Word8.fromInt rc);
+fun quit () = exit 0;
+
 use "ML-Systems/overloading_smlnj.ML";
 use "General/exn.ML";
 use "ML-Systems/single_assignment.ML";
@@ -50,9 +53,6 @@
 
 (* Poly/ML emulation *)
 
-val exit = exit o dest_int;
-fun quit () = exit 0;
-
 (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
 local
   val depth = ref (10: int);