refined option -W: output stream;
authorwenzelm
Thu Aug 28 19:29:56 2008 +0200 (2008-08-28)
changeset 280434d05f04cc671
parent 28042 1471f2974eb1
child 28044 e4b569b53e10
refined option -W: output stream;
bin/isabelle-process
     1.1 --- a/bin/isabelle-process	Thu Aug 28 17:54:18 2008 +0200
     1.2 +++ b/bin/isabelle-process	Thu Aug 28 19:29:56 2008 +0200
     1.3 @@ -32,7 +32,7 @@
     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 "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
     1.9    echo "    -c           tell ML system to compress output image"
    1.10    echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.11    echo "    -f           pass 'Session.finish();' to the ML session"
    1.12 @@ -65,7 +65,7 @@
    1.13  ISAR=false
    1.14  PROOFGENERAL=""
    1.15  SECURE=""
    1.16 -WRAPPER=""
    1.17 +WRAPPER_OUTPUT=""
    1.18  PGIP=""
    1.19  COMPRESS=""
    1.20  MLTEXT=""
    1.21 @@ -74,7 +74,7 @@
    1.22  READONLY=""
    1.23  NOWRITE=""
    1.24  
    1.25 -while getopts "CIPSWXce:fm:qruw" OPT
    1.26 +while getopts "CIPSW:Xce:fm:qruw" OPT
    1.27  do
    1.28    case "$OPT" in
    1.29      C)
    1.30 @@ -90,7 +90,7 @@
    1.31        SECURE=true
    1.32        ;;
    1.33      W)
    1.34 -      WRAPPER=true
    1.35 +      WRAPPER_OUTPUT="$OPTARG"
    1.36        ;;
    1.37      X)
    1.38        PGIP=true
    1.39 @@ -223,8 +223,8 @@
    1.40  [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
    1.41  
    1.42  NICE="nice"
    1.43 -if [ -n "$WRAPPER" ]; then
    1.44 -  MLTEXT="$MLTEXT; IsabelleProcess.init();"
    1.45 +if [ -n "$WRAPPER_OUTPUT" ]; then
    1.46 +  MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
    1.47  elif [ -n "$PGIP" ]; then
    1.48    MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
    1.49  elif [ -n "$PROOFGENERAL" ]; then