1.1 --- a/lib/scripts/run-polyml-5.0 Thu Aug 16 18:53:21 2007 +0200
1.2 +++ b/lib/scripts/run-polyml-5.0 Thu Aug 16 18:53:21 2007 +0200
1.3 @@ -52,15 +52,13 @@
1.4 EXIT=""
1.5 fi
1.6
1.7 -ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
1.8 -
1.9 if [ -z "$OUTFILE" ]; then
1.10 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
1.11 else
1.12 if [ -z "$COMPRESS" ]; then
1.13 - COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
1.14 + COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
1.15 else
1.16 - COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
1.17 + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
1.18 fi
1.19 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
1.20 rm -f "${OUTFILE}.o" || fail_out
2.1 --- a/lib/scripts/run-polyml-5.1 Thu Aug 16 18:53:21 2007 +0200
2.2 +++ b/lib/scripts/run-polyml-5.1 Thu Aug 16 18:53:21 2007 +0200
2.3 @@ -52,15 +52,13 @@
2.4 EXIT=""
2.5 fi
2.6
2.7 -ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
2.8 -
2.9 if [ -z "$OUTFILE" ]; then
2.10 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
2.11 else
2.12 if [ -z "$COMPRESS" ]; then
2.13 - COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
2.14 + COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
2.15 else
2.16 - COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
2.17 + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
2.18 fi
2.19 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
2.20 rm -f "${OUTFILE}.o" || fail_out
3.1 --- a/src/Pure/ML-Systems/polyml.ML Thu Aug 16 18:53:21 2007 +0200
3.2 +++ b/src/Pure/ML-Systems/polyml.ML Thu Aug 16 18:53:21 2007 +0200
3.3 @@ -111,7 +111,9 @@
3.4 fun eval "-q" = ()
3.5 | eval txt = use_text "" (println, println) false txt;
3.6 in
3.7 - val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
3.8 + val _ = PolyML.onEntry (fn () =>
3.9 + (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));
3.10 + app eval (CommandLine.arguments ())));
3.11 end;
3.12
3.13