equal
deleted
inserted
replaced
222 [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}" |
222 [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}" |
223 MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";" |
223 MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";" |
224 else |
224 else |
225 ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options" |
225 ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options" |
226 "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options" |
226 "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options" |
227 if [ "$INPUT" != RAW_ML_SYSTEM ]; then |
227 if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then |
228 MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT" |
228 MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT" |
229 fi |
229 fi |
230 if [ -n "$PROOFGENERAL" ]; then |
230 if [ -n "$PROOFGENERAL" ]; then |
231 MLTEXT="$MLTEXT; ProofGeneral.init ();" |
231 MLTEXT="$MLTEXT; ProofGeneral.init ();" |
232 elif [ -n "$ISAR" ]; then |
232 elif [ -n "$ISAR" ]; then |