author | wenzelm |
Fri, 01 Sep 2000 17:54:58 +0200 | |
changeset 9789 | 7e5e6c47c0b5 |
parent 5063 | d45ec8d00ab0 |
child 9977 | 32955afeb835 |
permissions | -rwxr-xr-x |
3007 | 1 |
#!/bin/bash |
2411 | 2 |
# |
3 |
# $Id$ |
|
9789 | 4 |
# Author: Markus Wenzel, TU Muenchen |
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
2411 | 6 |
# |
7 |
# SML/NJ startup script (for 0.93). |
|
8 |
# |
|
4333 | 9 |
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
2411 | 10 |
# and from settings |
11 |
||
12 |
||
13 |
## diagnostics |
|
14 |
||
15 |
function fail_out() |
|
16 |
{ |
|
17 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
|
18 |
exit 2 |
|
19 |
} |
|
20 |
||
5063 | 21 |
function check_mlhome_file() |
22 |
{ |
|
23 |
if [ ! -f "$1" ]; then |
|
24 |
echo "Unable to locate $1" >&2 |
|
25 |
echo "Please check your ML_HOME setting!" >&2 |
|
26 |
exit 2 |
|
27 |
fi |
|
28 |
} |
|
29 |
||
2411 | 30 |
|
31 |
## prepare databases |
|
32 |
||
2440 | 33 |
if [ -z "$INFILE" ]; then |
34 |
INFILE="$ML_HOME/sml" |
|
5063 | 35 |
check_mlhome_file "$INFILE" |
4513 | 36 |
EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;" |
2440 | 37 |
else |
38 |
EXIT="" |
|
39 |
fi |
|
2411 | 40 |
|
41 |
MOVE="" |
|
42 |
||
43 |
if [ -z "$OUTFILE" ]; then |
|
4513 | 44 |
COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);' |
2411 | 45 |
else |
46 |
if [ "$INFILE" -ef "$OUTFILE" ]; then |
|
47 |
OUTDIR=$(dirname "$OUTFILE")/tmp |
|
9789 | 48 |
OUTFILE="$OUTDIR"/$(basename "$OUTFILE") |
2411 | 49 |
mkdir -p "$OUTDIR" || fail_out |
50 |
MOVE=true |
|
51 |
fi |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2622
diff
changeset
|
52 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
2411 | 53 |
COMMIT="fun commit () = not (exportML\"$OUTFILE\");" |
54 |
fi |
|
55 |
||
56 |
||
57 |
## run it! |
|
58 |
||
4513 | 59 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
60 |
MLEXIT="commit();" |
|
2411 | 61 |
|
4513 | 62 |
if [ -z "$TERMINATE" ]; then |
63 |
FEEDER_OPTS="" |
|
2411 | 64 |
else |
4513 | 65 |
FEEDER_OPTS="-q" |
2411 | 66 |
fi |
67 |
||
9789 | 68 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
69 |
{ read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
70 |
RC="$?" |
|
4513 | 71 |
|
72 |
||
73 |
## fix heap file |
|
74 |
||
75 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
3503 | 76 |
|
2411 | 77 |
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then |
2551 | 78 |
rm -f "$INFILE" || fail_out |
79 |
mv "$OUTFILE" "$INFILE" || fail_out |
|
2411 | 80 |
fi |
81 |
||
9789 | 82 |
exit "$RC" |