Add -X option to trigger PGIP interaction mode.
--- a/bin/isabelle-process Fri May 07 12:47:44 2004 +0200
+++ b/bin/isabelle-process Fri May 07 13:34:13 2004 +0200
@@ -27,6 +27,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"
@@ -65,7 +66,7 @@
READONLY=""
NOWRITE=""
-while getopts "CIPce:fm:qruw" OPT
+while getopts "XCIPce:fm:qruw" OPT
do
case "$OPT" in
C)
@@ -77,6 +78,9 @@
P)
PROOFGENERAL=true
;;
+ X)
+ PGIP=true
+ ;;
c)
COMPRESS=true
;;
@@ -202,7 +206,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();"