bin/isabelle-process
changeset 45028 d608dd8cd409
parent 38253 3d4e521014f7
child 45056 bbd7eac14df3
equal deleted inserted replaced
45027:f459e93a038e 45028:d608dd8cd409
    27   echo
    27   echo
    28   echo "  Options are:"
    28   echo "  Options are:"
    29   echo "    -I           startup Isar interaction mode"
    29   echo "    -I           startup Isar interaction mode"
    30   echo "    -P           startup Proof General interaction mode"
    30   echo "    -P           startup Proof General interaction mode"
    31   echo "    -S           secure mode -- disallow critical operations"
    31   echo "    -S           secure mode -- disallow critical operations"
       
    32   echo "    -T ADDR      startup process wrapper, with socket address"
    32   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
    33   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
    33   echo "    -X           startup PGIP interaction mode"
    34   echo "    -X           startup PGIP interaction mode"
    34   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    35   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    35   echo "    -f           pass 'Session.finish();' to the ML session"
    36   echo "    -f           pass 'Session.finish();' to the ML session"
    36   echo "    -m MODE      add print mode for output"
    37   echo "    -m MODE      add print mode for output"
    59 # options
    60 # options
    60 
    61 
    61 ISAR=false
    62 ISAR=false
    62 PROOFGENERAL=""
    63 PROOFGENERAL=""
    63 SECURE=""
    64 SECURE=""
       
    65 WRAPPER_SOCKET=""
    64 WRAPPER_FIFOS=""
    66 WRAPPER_FIFOS=""
    65 PGIP=""
    67 PGIP=""
    66 MLTEXT=""
    68 MLTEXT=""
    67 MODES=""
    69 MODES=""
    68 TERMINATE=""
    70 TERMINATE=""
    69 READONLY=""
    71 READONLY=""
    70 NOWRITE=""
    72 NOWRITE=""
    71 
    73 
    72 while getopts "IPSW:Xe:fm:qruw" OPT
    74 while getopts "IPST:W:Xe:fm:qruw" OPT
    73 do
    75 do
    74   case "$OPT" in
    76   case "$OPT" in
    75     I)
    77     I)
    76       ISAR=true
    78       ISAR=true
    77       ;;
    79       ;;
    78     P)
    80     P)
    79       PROOFGENERAL=true
    81       PROOFGENERAL=true
    80       ;;
    82       ;;
    81     S)
    83     S)
    82       SECURE=true
    84       SECURE=true
       
    85       ;;
       
    86     T)
       
    87       WRAPPER_SOCKET="$OPTARG"
    83       ;;
    88       ;;
    84     W)
    89     W)
    85       WRAPPER_FIFOS="$OPTARG"
    90       WRAPPER_FIFOS="$OPTARG"
    86       ;;
    91       ;;
    87     X)
    92     X)
   211 
   216 
   212 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   217 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   213 
   218 
   214 NICE="nice"
   219 NICE="nice"
   215 
   220 
   216 if [ -n "$WRAPPER_FIFOS" ]; then
   221 if [ -n "$WRAPPER_SOCKET" ]; then
       
   222   MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
       
   223 elif [ -n "$WRAPPER_FIFOS" ]; then
   217   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   224   splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
   218   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   225   [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
   219   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   226   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   220   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   227   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   221   MLTEXT="$MLTEXT; Isabelle_Process.init \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
   228   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
   222 elif [ -n "$PGIP" ]; then
   229 elif [ -n "$PGIP" ]; then
   223   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   230   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   224 elif [ -n "$PROOFGENERAL" ]; then
   231 elif [ -n "$PROOFGENERAL" ]; then
   225   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   232   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   226 elif [ "$ISAR" = true ]; then
   233 elif [ "$ISAR" = true ]; then