bin/isabelle-process
changeset 51952 4517ceb545c1
parent 51948 cb5dbc9a06f9
child 51964 f1c1d8637216
equal deleted inserted replaced
51951:fab4ab92e812 51952:4517ceb545c1
   220   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   220   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   221   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   221   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   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   if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
   225   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   226     ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   226   "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
   227     "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
       
   228   fi
       
   229   if [ "$INPUT" != RAW_ML_SYSTEM ]; then
   227   if [ "$INPUT" != RAW_ML_SYSTEM ]; then
   230     MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
   228     MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
   231   fi
   229   fi
   232   if [ -n "$PROOFGENERAL" ]; then
   230   if [ -n "$PROOFGENERAL" ]; then
   233     MLTEXT="$MLTEXT; ProofGeneral.init ();"
   231     MLTEXT="$MLTEXT; ProofGeneral.init ();"