diff -r 7c517c92d315 -r f196352201d6 bin/isabelle-process
--- a/bin/isabelle-process	Sat May 11 18:16:17 2013 +0200
+++ b/bin/isabelle-process	Sat May 11 18:45:38 2013 +0200
@@ -31,7 +31,6 @@
   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 "    -X           startup PGIP interaction mode"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -f           pass 'Session.finish();' to the ML session"
   echo "    -m MODE      add print mode for output"
@@ -64,14 +63,13 @@
 SECURE=""
 WRAPPER_SOCKET=""
 WRAPPER_FIFOS=""
-PGIP=""
 MLTEXT=""
 MODES=""
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "IPST:W:Xe:fm:qruw" OPT
+while getopts "IPST:W:e:fm:qruw" OPT
 do
   case "$OPT" in
     I)
@@ -89,9 +87,6 @@
     W)
       WRAPPER_FIFOS="$OPTARG"
       ;;
-    X)
-      PGIP=true
-      ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
@@ -226,8 +221,6 @@
   [ -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 [ -n "$PGIP" ]; then
-  MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then
   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
 elif [ "$ISAR" = true ]; then