220 |
220 |
221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
222 |
222 |
223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" |
223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" |
224 |
224 |
|
225 NICE="nice" |
225 if [ -n "$WRAPPER" ]; then |
226 if [ -n "$WRAPPER" ]; then |
226 MLTEXT="$MLTEXT; IsabelleProcess.init();" |
227 MLTEXT="$MLTEXT; IsabelleProcess.init();" |
227 elif [ -n "$PGIP" ]; then |
228 elif [ -n "$PGIP" ]; then |
228 MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;" |
229 MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;" |
229 elif [ -n "$PROOFGENERAL" ]; then |
230 elif [ -n "$PROOFGENERAL" ]; then |
230 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
231 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
231 elif [ "$ISAR" = true ]; then |
232 elif [ "$ISAR" = true ]; then |
232 MLTEXT="$MLTEXT; Isar.main();" |
233 MLTEXT="$MLTEXT; Isar.main();" |
|
234 else |
|
235 NICE="" |
233 fi |
236 fi |
234 |
237 |
235 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \ |
238 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \ |
236 ISABELLE_PID ISABELLE_TMP |
239 ISABELLE_PID ISABELLE_TMP |
237 |
240 |
238 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
241 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
239 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
242 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
240 else |
243 else |
241 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |
244 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |
242 fi |
245 fi |
243 RC="$?" |
246 RC="$?" |
244 |
247 |
245 rmdir "$ISABELLE_TMP" |
248 rmdir "$ISABELLE_TMP" |
246 |
249 |