diff -r 98af3693f6b3 -r aed221aff642 bin/isabelle-process --- a/bin/isabelle-process Wed Apr 20 14:18:33 2005 +0200 +++ b/bin/isabelle-process Wed Apr 20 16:03:17 2005 +0200 @@ -1,7 +1,10 @@ #!/usr/bin/env bash # + # $Id$ + # Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) # # Isabelle process startup script. @@ -30,7 +33,6 @@ 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" @@ -69,7 +71,7 @@ READONLY="" NOWRITE="" -while getopts "XCIPce:fm:qruw" OPT +while getopts "CIPce:fm:qruw" OPT do case "$OPT" in C) @@ -81,9 +83,6 @@ P) PROOFGENERAL=true ;; - X) - PGIP=true - ;; c) COMPRESS=true ;; @@ -209,9 +208,7 @@ [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" -if [ -n "$PGIP" ]; then - MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;" -elif [ -n "$PROOFGENERAL" ]; then +if [ -n "$PROOFGENERAL" ]; then MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" elif [ "$ISAR" = true ]; then MLTEXT="$MLTEXT; Isar.main();"