bin/isabelle-process
changeset 14712 81362115cedd
parent 11550 915c5de6480f
child 14981 e73f8140af78
     1.1 --- a/bin/isabelle-process	Fri May 07 12:47:44 2004 +0200
     1.2 +++ b/bin/isabelle-process	Fri May 07 13:34:13 2004 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    echo "    -C           tell ML system to copy output image"
     1.5    echo "    -I           startup Isar interaction mode"
     1.6    echo "    -P           startup Proof General interaction mode"
     1.7 +  echo "    -X           startup PGIP interaction mode"
     1.8    echo "    -c           tell ML system to compress output image"
     1.9    echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.10    echo "    -f           pass 'Session.finish();' to the ML session"
    1.11 @@ -65,7 +66,7 @@
    1.12  READONLY=""
    1.13  NOWRITE=""
    1.14  
    1.15 -while getopts "CIPce:fm:qruw" OPT
    1.16 +while getopts "XCIPce:fm:qruw" OPT
    1.17  do
    1.18    case "$OPT" in
    1.19      C)
    1.20 @@ -77,6 +78,9 @@
    1.21      P)
    1.22        PROOFGENERAL=true
    1.23        ;;
    1.24 +    X)
    1.25 +      PGIP=true
    1.26 +      ;;
    1.27      c)
    1.28        COMPRESS=true
    1.29        ;;
    1.30 @@ -202,7 +206,9 @@
    1.31  
    1.32  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.33  
    1.34 -if [ -n "$PROOFGENERAL" ]; then
    1.35 +if [ -n "$PGIP" ]; then
    1.36 +  MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
    1.37 +elif [ -n "$PROOFGENERAL" ]; then
    1.38    MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
    1.39  elif [ "$ISAR" = true ]; then
    1.40    MLTEXT="$MLTEXT; Isar.main();"