48 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));" |
48 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));" |
49 EXIT="" |
49 EXIT="" |
50 fi |
50 fi |
51 |
51 |
52 if [ -z "$OUTFILE" ]; then |
52 if [ -z "$OUTFILE" ]; then |
53 COMMIT='fun commit () = false;' |
|
54 MLEXIT="" |
53 MLEXIT="" |
55 else |
54 else |
56 if [ -z "$INFILE" ]; then |
55 if [ -z "$INFILE" ]; then |
57 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);" |
56 MLEXIT="(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);" |
58 else |
57 else |
59 COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");" |
58 MLEXIT="Session.save \"$OUTFILE\";" |
60 fi |
59 fi |
61 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
60 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
62 MLEXIT="commit();" |
|
63 fi |
61 fi |
64 |
62 |
65 |
63 |
66 ## run it! |
64 ## run it! |
67 |
65 |
68 MLTEXT="$INIT $EXIT $COMMIT $MLTEXT" |
66 MLTEXT="$INIT $EXIT $MLTEXT" |
69 |
67 |
70 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then |
68 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then |
71 "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \ |
69 "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \ |
72 --error-exit </dev/null |
70 --error-exit </dev/null |
73 RC="$?" |
71 RC="$?" |