author | wenzelm |
Fri, 15 Sep 2000 16:31:36 +0200 | |
changeset 9977 | 32955afeb835 |
parent 9789 | 7e5e6c47c0b5 |
child 9997 | 38598a19e701 |
permissions | -rwxr-xr-x |
wenzelm@3007 | 1 |
#!/bin/bash |
wenzelm@2302 | 2 |
# |
wenzelm@2313 | 3 |
# $Id$ |
wenzelm@9789 | 4 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9789 | 5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@2313 | 6 |
# |
wenzelm@5708 | 7 |
# SML/NJ startup script (for 110 or later). |
wenzelm@9977 | 8 |
|
wenzelm@9977 | 9 |
export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP |
wenzelm@2302 | 10 |
|
wenzelm@2302 | 11 |
|
wenzelm@2302 | 12 |
## diagnostics |
wenzelm@2302 | 13 |
|
wenzelm@2349 | 14 |
function fail_out() |
wenzelm@2302 | 15 |
{ |
wenzelm@2349 | 16 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
wenzelm@2302 | 17 |
exit 2 |
wenzelm@2302 | 18 |
} |
wenzelm@2302 | 19 |
|
wenzelm@5063 | 20 |
function check_mlhome_file() |
wenzelm@5063 | 21 |
{ |
wenzelm@5063 | 22 |
if [ ! -f "$1" ]; then |
wenzelm@5063 | 23 |
echo "Unable to locate $1" >&2 |
wenzelm@5063 | 24 |
echo "Please check your ML_HOME setting!" >&2 |
wenzelm@5063 | 25 |
exit 2 |
wenzelm@5063 | 26 |
fi |
wenzelm@5063 | 27 |
} |
wenzelm@5063 | 28 |
|
wenzelm@6078 | 29 |
function check_heap_file() |
wenzelm@6078 | 30 |
{ |
wenzelm@6078 | 31 |
if [ ! -f "$1" ]; then |
wenzelm@6078 | 32 |
echo "Expected to find ML heap file $1" >&2 |
wenzelm@6078 | 33 |
return 1 |
wenzelm@6078 | 34 |
else |
wenzelm@6078 | 35 |
return 0 |
wenzelm@6078 | 36 |
fi |
wenzelm@6078 | 37 |
} |
wenzelm@6078 | 38 |
|
wenzelm@6078 | 39 |
|
wenzelm@5063 | 40 |
|
wenzelm@5063 | 41 |
## compiler binaries |
wenzelm@5063 | 42 |
|
wenzelm@5063 | 43 |
SML="$ML_HOME/sml" |
wenzelm@5063 | 44 |
ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys" |
wenzelm@5063 | 45 |
|
wenzelm@5063 | 46 |
check_mlhome_file "$SML" |
wenzelm@5063 | 47 |
check_mlhome_file "$ARCH_N_OPSYS" |
wenzelm@5063 | 48 |
|
wenzelm@5063 | 49 |
|
wenzelm@2302 | 50 |
|
wenzelm@2302 | 51 |
## prepare databases |
wenzelm@2302 | 52 |
|
wenzelm@4505 | 53 |
if [ -z "$INFILE" ]; then |
wenzelm@4505 | 54 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
wenzelm@4505 | 55 |
DB="" |
wenzelm@4505 | 56 |
else |
wenzelm@4505 | 57 |
EXIT="" |
wenzelm@3046 | 58 |
DB="@SMLload=$INFILE" |
wenzelm@2349 | 59 |
fi |
wenzelm@2349 | 60 |
|
wenzelm@4505 | 61 |
if [ -z "$OUTFILE" ]; then |
wenzelm@4505 | 62 |
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
wenzelm@4505 | 63 |
else |
wenzelm@4505 | 64 |
COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" |
wenzelm@4505 | 65 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
wenzelm@4505 | 66 |
fi |
wenzelm@2302 | 67 |
|
wenzelm@2302 | 68 |
|
wenzelm@2302 | 69 |
## run it! |
wenzelm@2302 | 70 |
|
wenzelm@4505 | 71 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
wenzelm@4505 | 72 |
MLEXIT="commit();" |
wenzelm@2302 | 73 |
|
wenzelm@4505 | 74 |
if [ -z "$TERMINATE" ]; then |
wenzelm@4505 | 75 |
FEEDER_OPTS="" |
wenzelm@2302 | 76 |
else |
wenzelm@4505 | 77 |
FEEDER_OPTS="-q" |
wenzelm@2302 | 78 |
fi |
wenzelm@2302 | 79 |
|
wenzelm@9789 | 80 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
wenzelm@9789 | 81 |
{ read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
wenzelm@9789 | 82 |
RC="$?" |
wenzelm@3046 | 83 |
|
wenzelm@4505 | 84 |
|
wenzelm@4505 | 85 |
## fix heap file name and permissions |
wenzelm@4505 | 86 |
|
wenzelm@4505 | 87 |
if [ -n "$OUTFILE" ]; then |
wenzelm@9789 | 88 |
eval $("$ARCH_N_OPSYS") |
wenzelm@6078 | 89 |
[ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS" |
wenzelm@6078 | 90 |
HEAP="$OUTFILE.$HEAP_SUFFIX" |
wenzelm@6078 | 91 |
check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \ |
wenzelm@4505 | 92 |
[ -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
wenzelm@4505 | 93 |
fi |
wenzelm@3503 | 94 |
|
wenzelm@9789 | 95 |
exit "$RC" |