bin/isabelle-process

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

   case "$OPT" in
     I)
       ISAR=true
       ;;
     P)
-      ISAR=true
       PROOFGENERAL=true
       ;;
     S)
       SECURE=true
       ;;

 
 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
 
 [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
 
-[ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
+[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
 
 NICE="nice"
 
 if [ -n "$WRAPPER_SOCKET" ]; then
   MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"

   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   [ -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]}\";"
-elif [ "$ISAR" = true ]; then
+else
   if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
     ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
     "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
   fi
+  if [ "$INPUT" != RAW_ML_SYSTEM ]; then
+    MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
+  fi
   if [ -n "$PROOFGENERAL" ]; then
     MLTEXT="$MLTEXT; ProofGeneral.init ();"
+  elif [ -n "$ISAR" ]; then
+    MLTEXT="$MLTEXT; Isar.main ();"
   else
-    MLTEXT="$MLTEXT; Isar.main ();"
+    NICE=""
   fi
-else
-  NICE=""
 fi
 
 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then