bin/isabelle_process

   echo
   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
   echo
   echo "  Options are:"
   echo "    -I           startup Isar interaction mode"
+  echo "    -O           system options from given YXML file"
   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
   echo "    -T ADDR      startup process wrapper, with socket address"
   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"

 ## process command line
 
 # options
 
 ISAR=""
+OPTIONS_FILE=""
 PROOFGENERAL=""
 SECURE=""
 WRAPPER_SOCKET=""
 WRAPPER_FIFOS=""
 MLTEXT=""

 declare -a SYSTEM_OPTIONS=()
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "IPST:W:e:m:o:qrw" OPT
+while getopts "IO:PST:W:e:m:o:qrw" OPT
 do
   case "$OPT" in
     I)
       ISAR=true
+      ;;
+    O)
+      OPTIONS_FILE="$OPTARG"
       ;;
     P)
       PROOFGENERAL=true
       ;;
     S)

   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
 else
   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
-  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
-    fail "Failed to retrieve Isabelle system options"
+  if [ -n "$OPTIONS_FILE" ]; then
+    [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \
+      fail "Cannot provide options file and options on command-line"
+    mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" ||
+      fail "Failed to move options file \"$OPTIONS_FILE\""
+  else
+    "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
+      fail "Failed to retrieve Isabelle system options"
+  fi
   if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
     MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
   fi
   if [ -n "$PROOFGENERAL" ]; then
     MLTEXT="$MLTEXT; ProofGeneral.init ();"