-P option;
authorwenzelm
Fri Sep 15 16:28:04 2000 +0200 (2000-09-15)
changeset 997205afcc505da3
parent 9971 e0164f01d55a
child 9973 d048e08f3347
-P option;
bin/isabelle
     1.1 --- a/bin/isabelle	Fri Sep 15 15:48:41 2000 +0200
     1.2 +++ b/bin/isabelle	Fri Sep 15 16:28:04 2000 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -I           startup Isar interaction mode"
     1.7 +  echo "    -P           startup ProofGeneral 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 "    -m MODE      add print mode for output"
    1.11 @@ -52,6 +53,8 @@
    1.12  
    1.13  # options
    1.14  
    1.15 +ISAR=false
    1.16 +PROOFGENERAL=""
    1.17  COMPRESS=""
    1.18  MLTEXT=""
    1.19  MODES=""
    1.20 @@ -59,11 +62,14 @@
    1.21  READONLY=""
    1.22  NOWRITE=""
    1.23  
    1.24 -while getopts "Ice:m:qruw" OPT
    1.25 +while getopts "IPce:m:qruw" OPT
    1.26  do
    1.27    case "$OPT" in
    1.28      I)
    1.29 -      MLTEXT="$MLTEXT Isar.main();"
    1.30 +      ISAR=true
    1.31 +      ;;
    1.32 +    P)
    1.33 +      PROOFGENERAL=true
    1.34        ;;
    1.35      c)
    1.36        COMPRESS=true
    1.37 @@ -187,6 +193,12 @@
    1.38  
    1.39  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.40  
    1.41 +if [ -n "$PROOFGENERAL" ]; then
    1.42 +  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
    1.43 +elif [ "$ISAR" = true ]; then
    1.44 +  MLTEXT="$MLTEXT; Isar.main();"
    1.45 +fi
    1.46 +
    1.47  export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
    1.48  
    1.49  if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then