bin/isabelle-process
changeset 15779 aed221aff642
parent 15778 98af3693f6b3
child 15784 3a214de33d53
--- 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();"