author | wenzelm |
Wed, 14 May 1997 18:37:03 +0200 | |
changeset 3184 | 4e0bbfb113d5 |
parent 3183 | 537f7281d42c |
child 3203 | af42c8cc8e75 |
permissions | -rwxr-xr-x |
3184 | 1 |
#!/usr/wiss/wenzelm/bin/bash |
2292 | 2 |
# |
2308 | 3 |
# $Id$ |
4 |
# |
|
2292 | 5 |
# Basic Isabelle startup script. |
6 |
||
7 |
||
8 |
## settings |
|
9 |
||
2704 | 10 |
PRG=$(basename $0) |
11 |
||
2735
29434f9b95dd
even more robust and user friendly invocation (no longer requieres
wenzelm
parents:
2711
diff
changeset
|
12 |
ISABELLE_HOME=$(dirname $0)/.. |
29434f9b95dd
even more robust and user friendly invocation (no longer requieres
wenzelm
parents:
2711
diff
changeset
|
13 |
. $ISABELLE_HOME/lib/scripts/getsettings || \ |
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2768
diff
changeset
|
14 |
{ echo "$PRG probably not called from its original place!"; exit 2; } |
2292 | 15 |
|
16 |
||
17 |
## diagnostics |
|
18 |
||
19 |
function usage() |
|
20 |
{ |
|
21 |
echo |
|
22 |
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
|
23 |
echo |
|
24 |
echo " Options are:" |
|
2343 | 25 |
echo " -e MLTEXT pass MLTEXT to the ML session" |
2704 | 26 |
echo " -m MODE add print mode for output" |
2292 | 27 |
echo " -q non-interactive session" |
28 |
echo " -r open heap file read-only" |
|
29 |
echo |
|
3184 | 30 |
echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
2292 | 31 |
echo " These are either names to be searched in the Isabelle path, or actual" |
2343 | 32 |
echo " file names (then containing at least one /)." |
2768 | 33 |
echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." |
2292 | 34 |
echo |
35 |
exit 1 |
|
36 |
} |
|
37 |
||
38 |
function fail() |
|
39 |
{ |
|
2343 | 40 |
echo "$1" >&2 |
2292 | 41 |
exit 2 |
42 |
} |
|
43 |
||
44 |
||
45 |
## process command line |
|
46 |
||
47 |
# options |
|
48 |
||
49 |
MLTEXT="" |
|
2704 | 50 |
MODES="" |
2292 | 51 |
TERMINATE="" |
52 |
READONLY="" |
|
53 |
||
3183 | 54 |
while getopts "e:m:qr" OPT |
2292 | 55 |
do |
56 |
case "$OPT" in |
|
57 |
e) |
|
58 |
MLTEXT="$MLTEXT $OPTARG" |
|
59 |
;; |
|
2704 | 60 |
m) |
61 |
if [ -z "$MODES" ]; then |
|
62 |
MODES="\"$OPTARG\"" |
|
63 |
else |
|
2711 | 64 |
MODES="\"$OPTARG\", $MODES" |
2704 | 65 |
fi |
66 |
;; |
|
2292 | 67 |
q) |
68 |
TERMINATE=true |
|
69 |
;; |
|
70 |
r) |
|
71 |
READONLY=true |
|
72 |
;; |
|
73 |
\?) |
|
74 |
usage |
|
75 |
;; |
|
76 |
esac |
|
77 |
done |
|
78 |
||
79 |
shift $(($OPTIND - 1)) |
|
80 |
||
81 |
||
82 |
# args |
|
83 |
||
84 |
INPUT="" |
|
85 |
OUTPUT="" |
|
86 |
||
87 |
if [ $# -ge 1 ]; then |
|
88 |
INPUT="$1" |
|
89 |
shift |
|
90 |
fi |
|
91 |
||
92 |
if [ $# -ge 1 ]; then |
|
93 |
OUTPUT="$1" |
|
94 |
shift |
|
95 |
fi |
|
96 |
||
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2768
diff
changeset
|
97 |
[ $# -ne 0 ] && { echo "Bad args: $*"; usage; } |
2292 | 98 |
|
99 |
||
100 |
## check ML system |
|
101 |
||
2308 | 102 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." |
2292 | 103 |
|
104 |
||
105 |
## input heap file |
|
106 |
||
3184 | 107 |
[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC" |
2292 | 108 |
|
109 |
case "$INPUT" in |
|
2768 | 110 |
RAW_ML_SYSTEM) |
2292 | 111 |
INFILE="" |
112 |
;; |
|
113 |
*/*) |
|
114 |
INFILE="$INPUT" |
|
2343 | 115 |
[ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |
2292 | 116 |
;; |
117 |
*) |
|
2308 | 118 |
ISA_PATH="" |
2292 | 119 |
INFILE="" |
120 |
for DIR in $(echo $ISABELLE_PATH | tr : " ") |
|
121 |
do |
|
2968 | 122 |
ISA_PATH="$ISA_PATH $DIR" |
123 |
[ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT |
|
2292 | 124 |
done |
2308 | 125 |
if [ -z "$INFILE" ]; then |
2343 | 126 |
echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 |
2308 | 127 |
for DIR in $ISA_PATH |
128 |
do |
|
2343 | 129 |
echo " $DIR" >&2 |
2308 | 130 |
done |
131 |
exit 2 |
|
132 |
fi |
|
2292 | 133 |
;; |
134 |
esac |
|
135 |
||
136 |
||
137 |
## output heap file |
|
138 |
||
139 |
case "$OUTPUT" in |
|
140 |
"") |
|
141 |
[ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE" |
|
142 |
;; |
|
143 |
*/*) |
|
144 |
OUTFILE="$OUTPUT" |
|
145 |
;; |
|
146 |
*) |
|
3118 | 147 |
mkdir -p "$ISABELLE_OUTPUT" |
148 |
OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
|
2292 | 149 |
;; |
150 |
esac |
|
151 |
||
152 |
||
153 |
## run it! |
|
154 |
||
155 |
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) |
|
156 |
||
2704 | 157 |
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
158 |
||
3054 | 159 |
export INFILE OUTFILE MLTEXT TERMINATE |
2292 | 160 |
[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM |
161 |
exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE |