4426
|
1 |
#!/bin/bash
|
|
2 |
#
|
|
3 |
# $Id$
|
9789
|
4 |
# Author: Markus Wenzel, TU Muenchen
|
|
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE)
|
4426
|
6 |
#
|
|
7 |
# MLWorks startup script (for 1.0r2 or later).
|
|
8 |
#
|
|
9 |
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
|
|
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 |
|
|
21 |
|
|
22 |
## prepare databases
|
|
23 |
|
|
24 |
if [ -z "$INFILE" ]; then
|
4505
|
25 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
|
4426
|
26 |
MLWORKS="mlworks-basis -tty"
|
|
27 |
else
|
4505
|
28 |
EXIT=""
|
9789
|
29 |
MLWORKS="mlimage -load \"$INFILE\" -tty"
|
4426
|
30 |
fi
|
|
31 |
|
4505
|
32 |
if [ -z "$OUTFILE" ]; then
|
|
33 |
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
|
|
34 |
else
|
|
35 |
COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);"
|
|
36 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
|
|
37 |
fi
|
4426
|
38 |
|
|
39 |
|
|
40 |
## run it!
|
|
41 |
|
4505
|
42 |
MLTEXT="$EXIT $COMMIT $MLTEXT"
|
|
43 |
MLEXIT="commit();"
|
4426
|
44 |
|
4505
|
45 |
if [ -z "$TERMINATE" ]; then
|
|
46 |
FEEDER_OPTS="-s"
|
4426
|
47 |
else
|
4505
|
48 |
FEEDER_OPTS="-q"
|
4426
|
49 |
fi
|
|
50 |
|
9789
|
51 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
|
|
52 |
{ read FPID; "$ML_HOME/$MLWORKS" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
|
|
53 |
RC="$?"
|
4505
|
54 |
|
|
55 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
|
4426
|
56 |
|
9789
|
57 |
exit "$RC"
|