author | wenzelm |
Thu, 23 Jan 1997 18:16:12 +0100 | |
changeset 2551 | fe15e3fcccf0 |
parent 2440 | b3ac45aba238 |
child 2622 | 80a81a36dd81 |
permissions | -rwxr-xr-x |
wenzelm@2411 | 1 |
#!/bin/bash -norc |
wenzelm@2411 | 2 |
# |
wenzelm@2411 | 3 |
# $Id$ |
wenzelm@2411 | 4 |
# |
wenzelm@2411 | 5 |
# SML/NJ startup script (for 0.93). |
wenzelm@2411 | 6 |
# |
wenzelm@2411 | 7 |
# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE, |
wenzelm@2411 | 8 |
# and from settings |
wenzelm@2411 | 9 |
|
wenzelm@2411 | 10 |
|
wenzelm@2411 | 11 |
## diagnostics |
wenzelm@2411 | 12 |
|
wenzelm@2411 | 13 |
function fail_out() |
wenzelm@2411 | 14 |
{ |
wenzelm@2411 | 15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
wenzelm@2411 | 16 |
exit 2 |
wenzelm@2411 | 17 |
} |
wenzelm@2411 | 18 |
|
wenzelm@2411 | 19 |
|
wenzelm@2411 | 20 |
## prepare databases |
wenzelm@2411 | 21 |
|
wenzelm@2440 | 22 |
if [ -z "$INFILE" ]; then |
wenzelm@2440 | 23 |
INFILE="$ML_HOME/sml" |
wenzelm@2440 | 24 |
EXIT="val exit = System.Unsafe.CInterface.exit;" |
wenzelm@2440 | 25 |
else |
wenzelm@2440 | 26 |
EXIT="" |
wenzelm@2440 | 27 |
fi |
wenzelm@2411 | 28 |
|
wenzelm@2411 | 29 |
MOVE="" |
wenzelm@2411 | 30 |
|
wenzelm@2411 | 31 |
if [ -z "$OUTFILE" ]; then |
wenzelm@2411 | 32 |
COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);' |
wenzelm@2411 | 33 |
else |
wenzelm@2411 | 34 |
if [ "$INFILE" -ef "$OUTFILE" ]; then |
wenzelm@2411 | 35 |
OUTDIR=$(dirname "$OUTFILE")/tmp |
wenzelm@2411 | 36 |
OUTFILE=$OUTDIR/$(basename "$OUTFILE") |
wenzelm@2411 | 37 |
mkdir -p "$OUTDIR" || fail_out |
wenzelm@2411 | 38 |
MOVE=true |
wenzelm@2411 | 39 |
fi |
wenzelm@2411 | 40 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out } |
wenzelm@2411 | 41 |
COMMIT="fun commit () = not (exportML\"$OUTFILE\");" |
wenzelm@2411 | 42 |
fi |
wenzelm@2411 | 43 |
|
wenzelm@2411 | 44 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
wenzelm@2411 | 45 |
MLEXIT="commit();" |
wenzelm@2411 | 46 |
|
wenzelm@2411 | 47 |
|
wenzelm@2411 | 48 |
## run it! |
wenzelm@2411 | 49 |
|
wenzelm@2411 | 50 |
START_SML="$INFILE $ML_OPTIONS" |
wenzelm@2411 | 51 |
|
wenzelm@2411 | 52 |
if [ -n "$TERMINATE" ]; then |
wenzelm@2411 | 53 |
{ echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML |
wenzelm@2411 | 54 |
RC=$? |
wenzelm@2411 | 55 |
else |
wenzelm@2411 | 56 |
{ echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML |
wenzelm@2411 | 57 |
RC=$? |
wenzelm@2411 | 58 |
fi |
wenzelm@2411 | 59 |
|
wenzelm@2411 | 60 |
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then |
wenzelm@2551 | 61 |
rm -f "$INFILE" || fail_out |
wenzelm@2551 | 62 |
mv "$OUTFILE" "$INFILE" || fail_out |
wenzelm@2411 | 63 |
fi |
wenzelm@2411 | 64 |
|
wenzelm@2411 | 65 |
exit $RC |