Add back rudely removed and popular -X option.
--- 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();"