author | wenzelm |
Thu, 06 May 2004 14:14:18 +0200 | |
changeset 14706 | 71590b7733b7 |
parent 11550 | 915c5de6480f |
child 14712 | 81362115cedd |
permissions | -rwxr-xr-x |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
2 |
# |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
3 |
# $Id$ |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
4 |
# Author: Markus Wenzel, TU Muenchen |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
6 |
# |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
7 |
# Isabelle process startup script. |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
8 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
9 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
10 |
## settings |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
11 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
12 |
PRG="$(basename "$0")" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
13 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
14 |
ISABELLE_HOME="$(dirname "$0")/.." |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
15 |
. "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
16 |
{ echo "$PRG probably not called from its original place!"; exit 2; } |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
17 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
18 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
19 |
## diagnostics |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
20 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
21 |
function usage() |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
22 |
{ |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
23 |
echo |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
24 |
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
25 |
echo |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
26 |
echo " Options are:" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
27 |
echo " -C tell ML system to copy output image" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
28 |
echo " -I startup Isar interaction mode" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
29 |
echo " -P startup Proof General interaction mode" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
30 |
echo " -c tell ML system to compress output image" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
31 |
echo " -e MLTEXT pass MLTEXT to the ML session" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
32 |
echo " -f pass 'Session.finish();' to the ML session" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
33 |
echo " -m MODE add print mode for output" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
34 |
echo " -q non-interactive session" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
35 |
echo " -r open heap file read-only" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
36 |
echo " -u pass 'use\"ROOT.ML\";' to the ML session" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
37 |
echo " -w reset write permissions on OUTPUT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
38 |
echo |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
39 |
echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
40 |
echo " These are either names to be searched in the Isabelle path, or" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
41 |
echo " actual file names (containing at least one /)." |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
42 |
echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
43 |
echo |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
44 |
exit 1 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
45 |
} |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
46 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
47 |
function fail() |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
48 |
{ |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
49 |
echo "$1" >&2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
50 |
exit 2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
51 |
} |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
52 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
53 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
54 |
## process command line |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
55 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
56 |
# options |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
57 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
58 |
COPYDB="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
59 |
ISAR=false |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
60 |
PROOFGENERAL="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
61 |
COMPRESS="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
62 |
MLTEXT="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
63 |
MODES="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
64 |
TERMINATE="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
65 |
READONLY="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
66 |
NOWRITE="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
67 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
68 |
while getopts "CIPce:fm:qruw" OPT |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
69 |
do |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
70 |
case "$OPT" in |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
71 |
C) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
72 |
COPYDB=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
73 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
74 |
I) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
75 |
ISAR=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
76 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
77 |
P) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
78 |
PROOFGENERAL=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
79 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
80 |
c) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
81 |
COMPRESS=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
82 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
83 |
e) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
84 |
MLTEXT="$MLTEXT $OPTARG" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
85 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
86 |
f) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
87 |
MLTEXT="$MLTEXT Session.finish();" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
88 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
89 |
m) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
90 |
if [ -z "$MODES" ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
91 |
MODES="\"$OPTARG\"" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
92 |
else |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
93 |
MODES="\"$OPTARG\", $MODES" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
94 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
95 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
96 |
q) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
97 |
TERMINATE=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
98 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
99 |
r) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
100 |
READONLY=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
101 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
102 |
u) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
103 |
MLTEXT="$MLTEXT use\"ROOT.ML\";" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
104 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
105 |
w) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
106 |
NOWRITE=true |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
107 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
108 |
\?) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
109 |
usage |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
110 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
111 |
esac |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
112 |
done |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
113 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
114 |
shift $(($OPTIND - 1)) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
115 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
116 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
117 |
# args |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
118 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
119 |
INPUT="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
120 |
OUTPUT="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
121 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
122 |
if [ "$#" -ge 1 ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
123 |
INPUT="$1" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
124 |
shift |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
125 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
126 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
127 |
if [ "$#" -ge 1 ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
128 |
OUTPUT="$1" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
129 |
shift |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
130 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
131 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
132 |
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
133 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
134 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
135 |
## check ML system |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
136 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
137 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
138 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
139 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
140 |
## input heap file |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
141 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
142 |
[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
143 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
144 |
case "$INPUT" in |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
145 |
RAW_ML_SYSTEM) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
146 |
INFILE="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
147 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
148 |
*/*) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
149 |
INFILE="$INPUT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
150 |
[ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
151 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
152 |
*) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
153 |
INFILE="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
154 |
ISA_PATH="" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
155 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
156 |
ORIG_IFS="$IFS" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
157 |
IFS=":" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
158 |
for DIR in $ISABELLE_PATH |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
159 |
do |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
160 |
DIR="$DIR/$ML_IDENTIFIER" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
161 |
ISA_PATH="$ISA_PATH $DIR\n" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
162 |
[ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
163 |
done |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
164 |
IFS="$ORIG_IFS" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
165 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
166 |
if [ -z "$INFILE" ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
167 |
echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
168 |
echo -ne "$ISA_PATH" >&2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
169 |
exit 2 |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
170 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
171 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
172 |
esac |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
173 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
174 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
175 |
## output heap file |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
176 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
177 |
case "$OUTPUT" in |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
178 |
"") |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
179 |
[ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
180 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
181 |
*/*) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
182 |
OUTFILE="$OUTPUT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
183 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
184 |
*) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
185 |
mkdir -p "$ISABELLE_OUTPUT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
186 |
OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
187 |
;; |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
188 |
esac |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
189 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
190 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
191 |
## prepare tmp directory |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
192 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
193 |
[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
194 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
195 |
ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
196 |
mkdir -p "$ISABELLE_TMP" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
197 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
198 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
199 |
## run it! |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
200 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
201 |
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
202 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
203 |
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
204 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
205 |
if [ -n "$PROOFGENERAL" ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
206 |
MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
207 |
elif [ "$ISAR" = true ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
208 |
MLTEXT="$MLTEXT; Isar.main();" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
209 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
210 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
211 |
export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
212 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
213 |
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
214 |
"$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
215 |
else |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
216 |
"$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
217 |
fi |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
218 |
RC="$?" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
219 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
220 |
rmdir "$ISABELLE_TMP" |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
221 |
|
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
diff
changeset
|
222 |
exit "$RC" |