Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more general exit;
authorwenzelm
Tue, 22 Apr 2014 11:47:57 +0200
changeset 56627 cb912b7de3cf
parent 56626 6532efd66a70
child 56628 a2df9de46060
more general exit;
lib/scripts/run-polyml file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.5.1 file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.5.2 file | annotate | diff | comparison | revisions
lib/scripts/run-smlnj file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/smlnj.ML file | annotate | diff | comparison | revisions 
--- 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));"
--- 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));"
--- 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));"
--- 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=""
--- 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);
isabelle