# HG changeset patch
# User wenzelm
# Date 1219944596 -7200
# Node ID 4d05f04cc671e0f2358943fde4f428a0459044bf
# Parent  1471f2974eb197c80ef37834ed6119c71fc6ddaa
refined option -W: output stream;

diff -r 1471f2974eb1 -r 4d05f04cc671 bin/isabelle-process
--- a/bin/isabelle-process	Thu Aug 28 17:54:18 2008 +0200
+++ b/bin/isabelle-process	Thu Aug 28 19:29:56 2008 +0200
@@ -32,7 +32,7 @@
   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
   echo "    -X           startup PGIP interaction mode"
-  echo "    -W           startup process wrapper (interaction via external program)"
+  echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
   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"
@@ -65,7 +65,7 @@
 ISAR=false
 PROOFGENERAL=""
 SECURE=""
-WRAPPER=""
+WRAPPER_OUTPUT=""
 PGIP=""
 COMPRESS=""
 MLTEXT=""
@@ -74,7 +74,7 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "CIPSWXce:fm:qruw" OPT
+while getopts "CIPSW:Xce:fm:qruw" OPT
 do
   case "$OPT" in
     C)
@@ -90,7 +90,7 @@
       SECURE=true
       ;;
     W)
-      WRAPPER=true
+      WRAPPER_OUTPUT="$OPTARG"
       ;;
     X)
       PGIP=true
@@ -223,8 +223,8 @@
 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
 
 NICE="nice"
-if [ -n "$WRAPPER" ]; then
-  MLTEXT="$MLTEXT; IsabelleProcess.init();"
+if [ -n "$WRAPPER_OUTPUT" ]; then
+  MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then