37 |
38 |
38 |
39 |
39 |
40 |
40 ## prepare databases |
41 ## prepare databases |
41 |
42 |
|
43 case "$ML_PLATFORM" in |
|
44 *-windows) |
|
45 PLATFORM_INFILE="$(platform_path -m "$INFILE")" |
|
46 PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")" |
|
47 ;; |
|
48 *) |
|
49 PLATFORM_INFILE="$INFILE" |
|
50 PLATFORM_OUTFILE="$OUTFILE" |
|
51 ;; |
|
52 esac |
|
53 |
42 if [ -z "$INFILE" ]; then |
54 if [ -z "$INFILE" ]; then |
43 INIT="" |
55 INIT="" |
44 EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" |
56 case "$ML_PLATFORM" in |
|
57 *-windows) |
|
58 EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));" |
|
59 ;; |
|
60 *) |
|
61 EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" |
|
62 ;; |
|
63 esac |
45 else |
64 else |
46 check_file "$INFILE" |
65 check_file "$INFILE" |
47 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));" |
66 INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));" |
48 EXIT="" |
67 EXIT="" |
49 fi |
68 fi |
50 |
69 |
51 if [ -z "$OUTFILE" ]; then |
70 if [ -z "$OUTFILE" ]; then |
52 MLEXIT="" |
71 MLEXIT="" |
53 else |
72 else |
54 if [ -z "$INFILE" ]; then |
73 if [ -z "$INFILE" ]; then |
55 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);" |
74 MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);" |
56 else |
75 else |
57 MLEXIT="Session.save \"$OUTFILE\";" |
76 MLEXIT="Session.save \"$OUTFILE\";" |
58 fi |
77 fi |
59 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
78 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
60 fi |
79 fi |
62 |
81 |
63 ## run it! |
82 ## run it! |
64 |
83 |
65 MLTEXT="$INIT $EXIT $MLTEXT" |
84 MLTEXT="$INIT $EXIT $MLTEXT" |
66 |
85 |
67 if [ -z "$TERMINATE" ]; then |
86 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then |
68 FEEDER_OPTS="" |
87 "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \ |
|
88 --error-exit </dev/null |
|
89 RC="$?" |
69 else |
90 else |
70 FEEDER_OPTS="-q" |
91 if [ -z "$TERMINATE" ]; then |
|
92 FEEDER_OPTS="" |
|
93 else |
|
94 FEEDER_OPTS="-q" |
|
95 ML_OPTIONS="$ML_OPTIONS --error-exit" |
|
96 fi |
|
97 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
98 { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
|
99 RC="$?" |
71 fi |
100 fi |
72 |
|
73 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
74 { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
|
75 RC="$?" |
|
76 |
101 |
77 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
102 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
78 |
103 |
79 exit "$RC" |
104 exit "$RC" |
80 |
105 |