25 echo |
25 echo |
26 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
26 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
27 echo |
27 echo |
28 echo " Options are:" |
28 echo " Options are:" |
29 echo " -I startup Isar interaction mode" |
29 echo " -I startup Isar interaction mode" |
|
30 echo " -O system options from given YXML file" |
30 echo " -P startup Proof General interaction mode" |
31 echo " -P startup Proof General interaction mode" |
31 echo " -S secure mode -- disallow critical operations" |
32 echo " -S secure mode -- disallow critical operations" |
32 echo " -T ADDR startup process wrapper, with socket address" |
33 echo " -T ADDR startup process wrapper, with socket address" |
33 echo " -W IN:OUT startup process wrapper, with input/output fifos" |
34 echo " -W IN:OUT startup process wrapper, with input/output fifos" |
34 echo " -e MLTEXT pass MLTEXT to the ML session" |
35 echo " -e MLTEXT pass MLTEXT to the ML session" |
218 [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}" |
223 [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}" |
219 [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}" |
224 [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}" |
220 MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";" |
225 MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";" |
221 else |
226 else |
222 ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options" |
227 ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options" |
223 "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \ |
228 if [ -n "$OPTIONS_FILE" ]; then |
224 fail "Failed to retrieve Isabelle system options" |
229 [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \ |
|
230 fail "Cannot provide options file and options on command-line" |
|
231 mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" || |
|
232 fail "Failed to move options file \"$OPTIONS_FILE\"" |
|
233 else |
|
234 "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \ |
|
235 fail "Failed to retrieve Isabelle system options" |
|
236 fi |
225 if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then |
237 if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then |
226 MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT" |
238 MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT" |
227 fi |
239 fi |
228 if [ -n "$PROOFGENERAL" ]; then |
240 if [ -n "$PROOFGENERAL" ]; then |
229 MLTEXT="$MLTEXT; ProofGeneral.init ();" |
241 MLTEXT="$MLTEXT; ProofGeneral.init ();" |