# HG changeset patch
# User aspinall
# Date 1117194692 -7200
# Node ID 37471d84d353c76b4267e28e94c5f5582211ad7a
# Parent  f80fc4bff9332e8db5b07865bfaee0e4e18c283b
Add back rudely removed and popular -X option.

diff -r f80fc4bff933 -r 37471d84d353 bin/isabelle-process
--- a/bin/isabelle-process	Fri May 27 12:12:05 2005 +0200
+++ b/bin/isabelle-process	Fri May 27 13:51:32 2005 +0200
@@ -30,6 +30,7 @@
   echo "    -C           tell ML system to copy output image"
   echo "    -I           startup Isar interaction mode"
   echo "    -P           startup Proof General interaction mode"
+  echo "    -X           startup PGIP interaction mode"
   echo "    -c           tell ML system to compress output image"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -f           pass 'Session.finish();' to the ML session"
@@ -68,7 +69,7 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "CIPce:fm:qruw" OPT
+while getopts "XCIPce:fm:qruw" OPT
 do
   case "$OPT" in
     C)
@@ -80,6 +81,9 @@
     P)
       PROOFGENERAL=true
       ;;
+    X)
+      PGIP=true
+      ;;
     c)
       COMPRESS=true
       ;;
@@ -205,7 +209,9 @@
 
 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
 
-if [ -n "$PROOFGENERAL" ]; then
+if [ -n "$PGIP" ]; then
+  MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
+elif [ -n "$PROOFGENERAL" ]; then
   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
 elif [ "$ISAR" = true ]; then
   MLTEXT="$MLTEXT; Isar.main();"