equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6 # |
|
7 # MLWorks startup script (for 1.0r2 or later). |
|
8 |
|
9 export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
|
10 |
|
11 |
|
12 ## diagnostics |
|
13 |
|
14 function fail_out() |
|
15 { |
|
16 echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
|
17 exit 2 |
|
18 } |
|
19 |
|
20 |
|
21 ## prepare databases |
|
22 |
|
23 if [ -z "$INFILE" ]; then |
|
24 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
|
25 MLWORKS="mlworks-basis -tty" |
|
26 else |
|
27 EXIT="" |
|
28 MLWORKS="mlimage -load $INFILE -tty" |
|
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 () = (Shell.saveImage (\"$OUTFILE\", false); true);" |
|
35 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
36 fi |
|
37 |
|
38 |
|
39 ## run it! |
|
40 |
|
41 MLTEXT="$EXIT $COMMIT $MLTEXT" |
|
42 MLEXIT="commit();" |
|
43 |
|
44 if [ -z "$TERMINATE" ]; then |
|
45 FEEDER_OPTS="" |
|
46 else |
|
47 FEEDER_OPTS="-q" |
|
48 fi |
|
49 |
|
50 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
51 { read FPID; "$ML_HOME"/$MLWORKS $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
52 RC="$?" |
|
53 |
|
54 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
55 |
|
56 exit "$RC" |
|