replaced option -p by -W (process wrapper);
authorwenzelm
Tue Dec 04 22:49:21 2007 +0100 (2007-12-04)
changeset 2552308b0feb07239
parent 25522 26851f8bdf14
child 25524 79f198a08c15
replaced option -p by -W (process wrapper);
tuned PGIP option setup;
bin/isabelle-process
     1.1 --- a/bin/isabelle-process	Tue Dec 04 21:09:37 2007 +0100
     1.2 +++ b/bin/isabelle-process	Tue Dec 04 22:49:21 2007 +0100
     1.3 @@ -32,11 +32,11 @@
     1.4    echo "    -P           startup Proof General interaction mode"
     1.5    echo "    -S           secure mode -- disallow critical operations"
     1.6    echo "    -X           startup PGIP interaction mode"
     1.7 +  echo "    -W           startup process wrapper (interaction via external program)"
     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    echo "    -m MODE      add print mode for output"
    1.12 -  echo "    -p           echo ISABELLE_PID on startup"
    1.13    echo "    -q           non-interactive session"
    1.14    echo "    -r           open heap file read-only"
    1.15    echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    1.16 @@ -65,15 +65,16 @@
    1.17  ISAR=false
    1.18  PROOFGENERAL=""
    1.19  SECURE=""
    1.20 +WRAPPER=""
    1.21 +PGIP=""
    1.22  COMPRESS=""
    1.23  MLTEXT=""
    1.24  MODES=""
    1.25 -ECHOPID=""
    1.26  TERMINATE=""
    1.27  READONLY=""
    1.28  NOWRITE=""
    1.29  
    1.30 -while getopts "XCIPSce:fm:pqruw" OPT
    1.31 +while getopts "CIPSWXce:fm:qruw" OPT
    1.32  do
    1.33    case "$OPT" in
    1.34      C)
    1.35 @@ -88,6 +89,9 @@
    1.36      S)
    1.37        SECURE=true
    1.38        ;;
    1.39 +    W)
    1.40 +      WRAPPER=true
    1.41 +      ;;
    1.42      X)
    1.43        PGIP=true
    1.44        ;;
    1.45 @@ -107,9 +111,6 @@
    1.46          MODES="\"$OPTARG\", $MODES"
    1.47        fi
    1.48        ;;
    1.49 -    p)
    1.50 -      ECHOPID=true
    1.51 -      ;;
    1.52      q)
    1.53        TERMINATE=true
    1.54        ;;
    1.55 @@ -221,7 +222,9 @@
    1.56  
    1.57  [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
    1.58  
    1.59 -if [ -n "$PGIP" ]; then
    1.60 +if [ -n "$WRAPPER" ]; then
    1.61 +  MLTEXT="$MLTEXT; IsabelleProcess.init();"
    1.62 +elif [ -n "$PGIP" ]; then
    1.63    MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
    1.64  elif [ -n "$PROOFGENERAL" ]; then
    1.65    MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
    1.66 @@ -232,8 +235,6 @@
    1.67  export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
    1.68    ISABELLE_PID ISABELLE_TMP
    1.69  
    1.70 -[ -n "$ECHOPID" ] && echo "ISABELLE_PID=$ISABELLE_PID"
    1.71 -
    1.72  if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
    1.73    "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
    1.74  else