# HG changeset patch # User aspinall # Date 1083929653 -7200 # Node ID 81362115cedd3424f0bfe11d5ef5028e05ae3910 # Parent 521aa281808a8e11bd08f332ac3970cf5e354544 Add -X option to trigger PGIP interaction mode. diff -r 521aa281808a -r 81362115cedd bin/isabelle-process --- 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();"