--- 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