author | wenzelm |
Sun, 28 Dec 1997 14:58:56 +0100 | |
changeset 4489 | 749600cb5573 |
parent 4333 | 1d326b826851 |
child 4513 | 6de428eac512 |
permissions | -rwxr-xr-x |
3007 | 1 |
#!/bin/bash |
2411 | 2 |
# |
3 |
# $Id$ |
|
4 |
# |
|
5 |
# SML/NJ startup script (for 0.93). |
|
6 |
# |
|
4333 | 7 |
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
2411 | 8 |
# and from settings |
9 |
||
10 |
||
11 |
## diagnostics |
|
12 |
||
13 |
function fail_out() |
|
14 |
{ |
|
15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
|
16 |
exit 2 |
|
17 |
} |
|
18 |
||
19 |
||
20 |
## prepare databases |
|
21 |
||
2440 | 22 |
if [ -z "$INFILE" ]; then |
23 |
INFILE="$ML_HOME/sml" |
|
24 |
EXIT="val exit = System.Unsafe.CInterface.exit;" |
|
25 |
else |
|
26 |
EXIT="" |
|
27 |
fi |
|
2411 | 28 |
|
29 |
MOVE="" |
|
30 |
||
31 |
if [ -z "$OUTFILE" ]; then |
|
2622
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2551
diff
changeset
|
32 |
COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\\n"); false);' |
2411 | 33 |
else |
34 |
if [ "$INFILE" -ef "$OUTFILE" ]; then |
|
35 |
OUTDIR=$(dirname "$OUTFILE")/tmp |
|
36 |
OUTFILE=$OUTDIR/$(basename "$OUTFILE") |
|
37 |
mkdir -p "$OUTDIR" || fail_out |
|
38 |
MOVE=true |
|
39 |
fi |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2622
diff
changeset
|
40 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
2411 | 41 |
COMMIT="fun commit () = not (exportML\"$OUTFILE\");" |
42 |
fi |
|
43 |
||
44 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
|
45 |
MLEXIT="commit();" |
|
46 |
||
47 |
||
48 |
## run it! |
|
49 |
||
50 |
START_SML="$INFILE $ML_OPTIONS" |
|
51 |
||
52 |
if [ -n "$TERMINATE" ]; then |
|
3010 | 53 |
echo "$MLTEXT" "$MLEXIT" | $START_SML |
2622
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2551
diff
changeset
|
54 |
RC=$? |
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2551
diff
changeset
|
55 |
elif [ -z "$MLTEXT" ]; then |
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2551
diff
changeset
|
56 |
sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
2411 | 57 |
RC=$? |
58 |
else |
|
2622
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2551
diff
changeset
|
59 |
sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
2411 | 60 |
RC=$? |
61 |
fi |
|
62 |
||
3503 | 63 |
[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
64 |
||
2411 | 65 |
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then |
2551 | 66 |
rm -f "$INFILE" || fail_out |
67 |
mv "$OUTFILE" "$INFILE" || fail_out |
|
2411 | 68 |
fi |
69 |
||
70 |
exit $RC |