lib/scripts/run-polyml
changeset 51099 2ef891f99d2c
parent 48662 b171bcd5dd86
child 52831 72bbdc64d0de
equal deleted inserted replaced
51098:22d5c010ef5c 51099:2ef891f99d2c
    47 if [ -z "$INFILE" ]; then
    47 if [ -z "$INFILE" ]; then
    48   INIT=""
    48   INIT=""
    49   EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
    49   EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
    50 else
    50 else
    51   check_file "$INFILE"
    51   check_file "$INFILE"
    52   INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
    52   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));"
    53   EXIT=""
    53   EXIT=""
    54 fi
    54 fi
    55 
    55 
    56 if [ -z "$OUTFILE" ]; then
    56 if [ -z "$OUTFILE" ]; then
    57   COMMIT='fun commit () = false;'
    57   COMMIT='fun commit () = false;'
    58   MLEXIT=""
    58   MLEXIT=""
    59 else
    59 else
    60   COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
    60   COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
    61   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    61   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    62   MLEXIT="commit();"
    62   MLEXIT="commit();"
    63 fi
    63 fi
    64 
    64 
    65 
    65