equal
deleted
inserted
replaced
151 case "$INPUT" in |
151 case "$INPUT" in |
152 RAW_ML_SYSTEM) |
152 RAW_ML_SYSTEM) |
153 INFILE="" |
153 INFILE="" |
154 ;; |
154 ;; |
155 */*) |
155 */*) |
156 INFILE="$INPUT" |
156 INFILE="$INPUT$ML_SUFFIX" |
157 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |
157 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |
158 ;; |
158 ;; |
159 *) |
159 *) |
160 INFILE="" |
160 INFILE="" |
161 ISA_PATH="" |
161 ISA_PATH="" |
164 IFS=":" |
164 IFS=":" |
165 for DIR in $ISABELLE_PATH |
165 for DIR in $ISABELLE_PATH |
166 do |
166 do |
167 DIR="$DIR/$ML_IDENTIFIER" |
167 DIR="$DIR/$ML_IDENTIFIER" |
168 ISA_PATH="$ISA_PATH $DIR\n" |
168 ISA_PATH="$ISA_PATH $DIR\n" |
169 [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT" |
169 [ -z "$INFILE" -a -f "$DIR/$INPUT$ML_SUFFIX" ] && INFILE="$DIR/$INPUT$ML_SUFFIX" |
170 done |
170 done |
171 IFS="$ORIG_IFS" |
171 IFS="$ORIG_IFS" |
172 |
172 |
173 if [ -z "$INFILE" ]; then |
173 if [ -z "$INFILE" ]; then |
174 echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 |
174 echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 |
184 case "$OUTPUT" in |
184 case "$OUTPUT" in |
185 "") |
185 "") |
186 [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE" |
186 [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE" |
187 ;; |
187 ;; |
188 */*) |
188 */*) |
189 OUTFILE="$OUTPUT" |
189 OUTFILE="$OUTPUT$ML_SUFFIX" |
190 ;; |
190 ;; |
191 *) |
191 *) |
192 mkdir -p "$ISABELLE_OUTPUT" |
192 mkdir -p "$ISABELLE_OUTPUT" |
193 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
193 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT$ML_SUFFIX" |
194 ;; |
194 ;; |
195 esac |
195 esac |
196 |
196 |
197 |
197 |
198 ## prepare tmp directory |
198 ## prepare tmp directory |
199 |
199 |
200 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
200 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
201 ISABELLE_PID="$$" |
201 ISABELLE_PID="$$" |
202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX${ISABELLE_PID}" |
202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
203 mkdir -p "$ISABELLE_TMP" |
203 mkdir -p "$ISABELLE_TMP" |
204 |
204 |
205 |
205 |
206 ## run it! |
206 ## run it! |
207 |
207 |