author | wenzelm |
Mon, 18 Sep 2000 14:49:51 +0200 | |
changeset 10017 | e146bbfc38c1 |
parent 9997 | 38598a19e701 |
child 10105 | f9be78009930 |
permissions | -rwxr-xr-x |
3007 | 1 |
#!/bin/bash |
2301 | 2 |
# |
2314 | 3 |
# $Id$ |
9789 | 4 |
# Author: Markus Wenzel, TU Muenchen |
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
2314 | 6 |
# |
2301 | 7 |
# Poly/ML startup script. |
9977 | 8 |
|
9997 | 9 |
export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE |
2301 | 10 |
|
11 |
||
12 |
## diagnostics |
|
13 |
||
2349 | 14 |
function fail_out() |
2301 | 15 |
{ |
2349 | 16 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
2301 | 17 |
exit 2 |
18 |
} |
|
19 |
||
5063 | 20 |
function check_mlhome_file() |
21 |
{ |
|
22 |
if [ ! -f "$1" ]; then |
|
23 |
echo "Unable to locate $1" >&2 |
|
24 |
echo "Please check your ML_HOME setting!" >&2 |
|
25 |
exit 2 |
|
26 |
fi |
|
27 |
} |
|
28 |
||
2301 | 29 |
|
2400 | 30 |
## Poly/ML programs |
2301 | 31 |
|
9789 | 32 |
POLY="$ML_HOME/poly" |
33 |
DISCGARB="$ML_HOME/discgarb" |
|
2301 | 34 |
|
5063 | 35 |
check_mlhome_file "$POLY" |
36 |
check_mlhome_file "$DISCGARB" |
|
37 |
||
2301 | 38 |
|
9765 | 39 |
case "$ML_SYSTEM" in |
40 |
polyml-4.*) |
|
41 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
|
42 |
;; |
|
43 |
*) |
|
44 |
EXIT="val exit = PolyML.exit;" |
|
45 |
;; |
|
46 |
esac |
|
47 |
||
48 |
||
2301 | 49 |
## prepare databases |
50 |
||
3055 | 51 |
COPYDB=true |
2349 | 52 |
|
2301 | 53 |
if [ -z "$INFILE" ]; then |
2400 | 54 |
INFILE="$ML_HOME/ML_dbase" |
5063 | 55 |
check_mlhome_file "$INFILE" |
3055 | 56 |
COPYDB="" |
9765 | 57 |
MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
2301 | 58 |
fi |
59 |
||
60 |
if [ -z "$OUTFILE" ]; then |
|
61 |
DB="$INFILE" |
|
2349 | 62 |
ML_OPTIONS="-r $ML_OPTIONS" |
63 |
elif [ "$INFILE" -ef "$OUTFILE" ]; then |
|
2301 | 64 |
DB="$INFILE" |
65 |
elif [ -n "$COPYDB" ]; then |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2605
diff
changeset
|
66 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
2548 | 67 |
cp "$INFILE" "$OUTFILE" || fail_out |
2349 | 68 |
chmod +w "$OUTFILE" || fail_out |
2301 | 69 |
DB="$OUTFILE" |
70 |
else |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2605
diff
changeset
|
71 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
9789 | 72 |
echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" |
2301 | 73 |
[ -f "$OUTFILE" ] || fail_out |
74 |
DB="$OUTFILE" |
|
75 |
fi |
|
76 |
||
77 |
||
78 |
## run it! |
|
79 |
||
4505 | 80 |
if [ -z "$TERMINATE" ]; then |
81 |
FEEDER_OPTS="-s" |
|
82 |
else |
|
83 |
FEEDER_OPTS="-q" |
|
84 |
fi |
|
85 |
||
2400 | 86 |
DB_INFO=$(ls -l "$DB") |
2349 | 87 |
|
9789 | 88 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
89 |
{ read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
90 |
RC="$?" |
|
2301 | 91 |
|
2400 | 92 |
NEW_DB_INFO=$(ls -l "$DB") |
9789 | 93 |
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE" |
4505 | 94 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
2301 | 95 |
|
9789 | 96 |
exit "$RC" |