removed signal setup from root function to on-entry hook;
authorwenzelm
Thu, 16 Aug 2007 18:53:21 +0200
changeset 242963479a9fe73e0
parent 24295 af8dbc7a2305
child 24297 a50cdc42798d
removed signal setup from root function to on-entry hook;
lib/scripts/run-polyml-5.0
lib/scripts/run-polyml-5.1
src/Pure/ML-Systems/polyml.ML
     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