author | wenzelm |
Sat, 20 Dec 2008 11:55:34 +0100 | |
changeset 29145 | b1c6f4563df7 |
parent 14981 | e73f8140af78 |
child 31315 | 3c7b40548a84 |
permissions | -rwxr-xr-x |
wenzelm@10555 | 1 |
#!/usr/bin/env bash |
wenzelm@9253 | 2 |
# |
wenzelm@9789 | 3 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9253 | 4 |
# |
wenzelm@9253 | 5 |
# Moscow ML 2.00 startup script |
wenzelm@9977 | 6 |
|
wenzelm@10105 | 7 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
wenzelm@9253 | 8 |
|
wenzelm@9253 | 9 |
|
wenzelm@9253 | 10 |
## diagnostics |
wenzelm@9253 | 11 |
|
wenzelm@9253 | 12 |
function fail_out() |
wenzelm@9253 | 13 |
{ |
wenzelm@9253 | 14 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
wenzelm@9253 | 15 |
exit 2 |
wenzelm@9253 | 16 |
} |
wenzelm@9253 | 17 |
|
wenzelm@9253 | 18 |
|
wenzelm@9253 | 19 |
## prepare databases |
wenzelm@9253 | 20 |
|
wenzelm@9253 | 21 |
MOSML="mosml -P sml90" |
wenzelm@9253 | 22 |
|
wenzelm@9253 | 23 |
if [ -z "$INFILE" ]; then |
wenzelm@9253 | 24 |
EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;' |
wenzelm@9253 | 25 |
else |
wenzelm@9253 | 26 |
EXIT="" |
wenzelm@9253 | 27 |
echo "Cannot load images yet!" >&2 |
wenzelm@9253 | 28 |
exit 2 |
wenzelm@9253 | 29 |
fi |
wenzelm@9253 | 30 |
|
wenzelm@9253 | 31 |
if [ -z "$OUTFILE" ]; then |
wenzelm@9253 | 32 |
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
wenzelm@9253 | 33 |
else |
wenzelm@9253 | 34 |
COMMIT="fun commit () = true;" |
wenzelm@9253 | 35 |
echo "WARNING: cannot save images yet!" >&2 |
wenzelm@9253 | 36 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
wenzelm@9253 | 37 |
fi |
wenzelm@9253 | 38 |
|
wenzelm@9253 | 39 |
|
wenzelm@9253 | 40 |
## run it! |
wenzelm@9253 | 41 |
|
wenzelm@9253 | 42 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
wenzelm@9253 | 43 |
MLEXIT="commit();" |
wenzelm@9253 | 44 |
|
wenzelm@9253 | 45 |
if [ -z "$TERMINATE" ]; then |
wenzelm@9253 | 46 |
FEEDER_OPTS="" |
wenzelm@9253 | 47 |
else |
wenzelm@9253 | 48 |
FEEDER_OPTS="-q" |
wenzelm@9253 | 49 |
fi |
wenzelm@9253 | 50 |
|
wenzelm@9789 | 51 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
wenzelm@9794 | 52 |
{ read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
wenzelm@9789 | 53 |
RC="$?" |
wenzelm@9253 | 54 |
|
wenzelm@9253 | 55 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
wenzelm@9253 | 56 |
|
wenzelm@9789 | 57 |
exit "$RC" |