bin/isabelle-process
changeset 45028 d608dd8cd409
parent 38253 3d4e521014f7
child 45056 bbd7eac14df3
     1.1 --- a/bin/isabelle-process	Wed Sep 21 20:35:50 2011 +0200
     1.2 +++ b/bin/isabelle-process	Wed Sep 21 22:18:17 2011 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    echo "    -I           startup Isar interaction mode"
     1.5    echo "    -P           startup Proof General interaction mode"
     1.6    echo "    -S           secure mode -- disallow critical operations"
     1.7 +  echo "    -T ADDR      startup process wrapper, with socket address"
     1.8    echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
     1.9    echo "    -X           startup PGIP interaction mode"
    1.10    echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.11 @@ -61,6 +62,7 @@
    1.12  ISAR=false
    1.13  PROOFGENERAL=""
    1.14  SECURE=""
    1.15 +WRAPPER_SOCKET=""
    1.16  WRAPPER_FIFOS=""
    1.17  PGIP=""
    1.18  MLTEXT=""
    1.19 @@ -69,7 +71,7 @@
    1.20  READONLY=""
    1.21  NOWRITE=""
    1.22  
    1.23 -while getopts "IPSW:Xe:fm:qruw" OPT
    1.24 +while getopts "IPST:W:Xe:fm:qruw" OPT
    1.25  do
    1.26    case "$OPT" in
    1.27      I)
    1.28 @@ -81,6 +83,9 @@
    1.29      S)
    1.30        SECURE=true
    1.31        ;;
    1.32 +    T)
    1.33 +      WRAPPER_SOCKET="$OPTARG"
    1.34 +      ;;
    1.35      W)
    1.36        WRAPPER_FIFOS="$OPTARG"
    1.37        ;;
    1.38 @@ -213,12 +218,14 @@
    1.39  
    1.40  NICE="nice"
    1.41  
    1.42 -if [ -n "$WRAPPER_FIFOS" ]; then
    1.43 +if [ -n "$WRAPPER_SOCKET" ]; then
    1.44 +  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
    1.45 +elif [ -n "$WRAPPER_FIFOS" ]; then
    1.46    splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
    1.47    [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
    1.48    [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
    1.49    [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
    1.50 -  MLTEXT="$MLTEXT; Isabelle_Process.init \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
    1.51 +  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
    1.52  elif [ -n "$PGIP" ]; then
    1.53    MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
    1.54  elif [ -n "$PROOFGENERAL" ]; then