# 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);