diff -r e0164f01d55a -r 05afcc505da3 bin/isabelle
--- a/bin/isabelle	Fri Sep 15 15:48:41 2000 +0200
+++ b/bin/isabelle	Fri Sep 15 16:28:04 2000 +0200
@@ -25,6 +25,7 @@
   echo
   echo "  Options are:"
   echo "    -I           startup Isar interaction mode"
+  echo "    -P           startup ProofGeneral interaction mode"
   echo "    -c           tell ML system to compress output image"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -m MODE      add print mode for output"
@@ -52,6 +53,8 @@
 
 # options
 
+ISAR=false
+PROOFGENERAL=""
 COMPRESS=""
 MLTEXT=""
 MODES=""
@@ -59,11 +62,14 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "Ice:m:qruw" OPT
+while getopts "IPce:m:qruw" OPT
 do
   case "$OPT" in
     I)
-      MLTEXT="$MLTEXT Isar.main();"
+      ISAR=true
+      ;;
+    P)
+      PROOFGENERAL=true
       ;;
     c)
       COMPRESS=true
@@ -187,6 +193,12 @@
 
 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
 
+if [ -n "$PROOFGENERAL" ]; then
+  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
+elif [ "$ISAR" = true ]; then
+  MLTEXT="$MLTEXT; Isar.main();"
+fi
+
 export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then