equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Markus Wenzel, TU Muenchen |
|
4 # |
|
5 # Moscow ML 2.00 startup script |
|
6 |
|
7 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE |
|
8 |
|
9 |
|
10 ## diagnostics |
|
11 |
|
12 function fail_out() |
|
13 { |
|
14 echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
|
15 exit 2 |
|
16 } |
|
17 |
|
18 |
|
19 ## prepare databases |
|
20 |
|
21 MOSML="mosml -P sml90" |
|
22 |
|
23 if [ -z "$INFILE" ]; then |
|
24 EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;' |
|
25 else |
|
26 EXIT="" |
|
27 echo "Cannot load images yet!" >&2 |
|
28 exit 2 |
|
29 fi |
|
30 |
|
31 if [ -z "$OUTFILE" ]; then |
|
32 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
|
33 else |
|
34 COMMIT="fun commit () = true;" |
|
35 echo "WARNING: cannot save images yet!" >&2 |
|
36 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
37 fi |
|
38 |
|
39 |
|
40 ## run it! |
|
41 |
|
42 MLTEXT="$EXIT $COMMIT $MLTEXT" |
|
43 MLEXIT="commit();" |
|
44 |
|
45 if [ -z "$TERMINATE" ]; then |
|
46 FEEDER_OPTS="" |
|
47 else |
|
48 FEEDER_OPTS="-q" |
|
49 fi |
|
50 |
|
51 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
52 { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
53 RC="$?" |
|
54 |
|
55 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
56 |
|
57 exit "$RC" |
|