--- 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