bin/isabelle_process

   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"
   echo "    -m MODE      add print mode for output"

 
 # options
 
 ISAR=""
 OPTIONS_FILE=""
-PROOFGENERAL=""
 SECURE=""
 WRAPPER_SOCKET=""
 WRAPPER_FIFOS=""
 MLTEXT=""
 MODES=""
 declare -a SYSTEM_OPTIONS=()
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "IO:PST:W:e:m:o:qrw" OPT
+while getopts "IO:ST:W:e:m:o:qrw" OPT
 do
   case "$OPT" in
     I)
       ISAR=true
       ;;
     O)
       OPTIONS_FILE="$OPTARG"
-      ;;
-    P)
-      PROOFGENERAL=true
       ;;
     S)
       SECURE=true
       ;;
     T)

       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 ();"
-  elif [ -n "$ISAR" ]; then
+  if [ -n "$ISAR" ]; then
     MLTEXT="$MLTEXT; Isar.main ();"
   else
     NICE=""
   fi
 fi