bin/isabelle-process

--- a/bin/isabelle-process	Wed Sep 21 20:35:50 2011 +0200
+++ b/bin/isabelle-process	Wed Sep 21 22:18:17 2011 +0200
@@ -29,6 +29,7 @@
   echo "    -I           startup Isar interaction mode"
   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
+  echo "    -T ADDR      startup process wrapper, with socket address"
   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -X           startup PGIP interaction mode"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
@@ -61,6 +62,7 @@
 ISAR=false
 PROOFGENERAL=""
 SECURE=""
+WRAPPER_SOCKET=""
 WRAPPER_FIFOS=""
 PGIP=""
 MLTEXT=""
@@ -69,7 +71,7 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "IPSW:Xe:fm:qruw" OPT
+while getopts "IPST:W:Xe:fm:qruw" OPT
 do
   case "$OPT" in
     I)
@@ -81,6 +83,9 @@
     S)
       SECURE=true
       ;;
+    T)
+      WRAPPER_SOCKET="$OPTARG"
+      ;;
     W)
       WRAPPER_FIFOS="$OPTARG"
       ;;
@@ -213,12 +218,14 @@
 
 NICE="nice"
 
-if [ -n "$WRAPPER_FIFOS" ]; then
+if [ -n "$WRAPPER_SOCKET" ]; then
+  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
+elif [ -n "$WRAPPER_FIFOS" ]; then
   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
-  MLTEXT="$MLTEXT; Isabelle_Process.init \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
+  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then