author | wenzelm |
Mon, 07 Jul 1997 09:06:26 +0200 | |
changeset 3503 | 390093b95cb0 |
parent 3055 | 5da4afa207ad |
child 3630 | aee7effe0816 |
permissions | -rwxr-xr-x |
3007 | 1 |
#!/bin/bash |
2302 | 2 |
# |
2313 | 3 |
# $Id$ |
4 |
# |
|
2302 | 5 |
# SML/NJ startup script (for 1.06 or later). |
6 |
# |
|
3503 | 7 |
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE, |
2302 | 8 |
# and from settings |
9 |
||
10 |
||
11 |
## diagnostics |
|
12 |
||
2349 | 13 |
function fail_out() |
2302 | 14 |
{ |
2349 | 15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
2302 | 16 |
exit 2 |
17 |
} |
|
18 |
||
19 |
||
3046 | 20 |
## version specific stuff |
2302 | 21 |
|
2349 | 22 |
EXIT="" |
3046 | 23 |
COMMIT="" |
3051 | 24 |
SUFFIX="" |
3046 | 25 |
|
26 |
case "$ML_SYSTEM" in |
|
27 |
smlnj-1.0[678]*) |
|
28 |
EXIT="val exit = System.Unix.exit;" |
|
29 |
COMMIT="fun commit () = not (exportML\"$OUTFILE\");" |
|
30 |
COMMIT_RO='fun commit () = (output (std_err, "Error - Database is not opened for writing.\\n"); false);' |
|
2349 | 31 |
;; |
3046 | 32 |
smlnj-1.09*) |
33 |
EXIT="fun exit 0 : unit = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;" |
|
34 |
COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" |
|
35 |
COMMIT_RO='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\\n"); false);' |
|
3051 | 36 |
eval $($ML_HOME/.arch-n-opsys) |
37 |
SUFFIX=".$ARCH-$OPSYS" |
|
3046 | 38 |
;; |
39 |
esac |
|
40 |
||
41 |
||
42 |
## prepare databases |
|
43 |
||
44 |
DB="$INFILE" |
|
45 |
||
46 |
if [ -n "$DB" ]; then |
|
47 |
DB="@SMLload=$INFILE" |
|
48 |
EXIT="" |
|
2349 | 49 |
fi |
50 |
||
3051 | 51 |
[ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO" |
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2622
diff
changeset
|
52 |
[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
2396 | 53 |
|
2349 | 54 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
3046 | 55 |
MLEXIT="commit ();" |
2302 | 56 |
|
57 |
||
58 |
## run it! |
|
59 |
||
2429 | 60 |
START_SML="$ML_HOME/sml $ML_OPTIONS $DB" |
2302 | 61 |
|
62 |
if [ -n "$TERMINATE" ]; then |
|
3051 | 63 |
sh -c "echo '$MLTEXT' '$MLEXIT' | $START_SML" |
2622
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2429
diff
changeset
|
64 |
RC=$? |
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2429
diff
changeset
|
65 |
elif [ -z "$MLTEXT" ]; then |
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2429
diff
changeset
|
66 |
sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
2302 | 67 |
RC=$? |
68 |
else |
|
2622
80a81a36dd81
semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents:
2429
diff
changeset
|
69 |
sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
2302 | 70 |
RC=$? |
71 |
fi |
|
72 |
||
3046 | 73 |
#fix heap file name |
3051 | 74 |
[ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \ |
75 |
&& mv "$OUTFILE$SUFFIX" "$OUTFILE" |
|
3046 | 76 |
|
3503 | 77 |
[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
78 |
||
2302 | 79 |
exit $RC |