equal
deleted
inserted
replaced
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 |
201 ISABELLE_PID="$$" |
202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$" |
202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX${ISABELLE_PID}" |
203 mkdir -p "$ISABELLE_TMP" |
203 mkdir -p "$ISABELLE_TMP" |
|
204 |
204 |
205 |
205 ## run it! |
206 ## run it! |
206 |
207 |
207 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
208 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
208 |
209 |
214 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
215 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
215 elif [ "$ISAR" = true ]; then |
216 elif [ "$ISAR" = true ]; then |
216 MLTEXT="$MLTEXT; Isar.main();" |
217 MLTEXT="$MLTEXT; Isar.main();" |
217 fi |
218 fi |
218 |
219 |
219 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP |
220 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \ |
220 export ISABELLE_PID="$$" |
221 ISABELLE_PID ISABELLE_TMP |
221 |
222 |
222 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
223 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
223 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
224 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
224 else |
225 else |
225 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |
226 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |