bin/isabelle-process
changeset 51932 f196352201d6
parent 51312 0ce544fbb509
child 51938 cf9c8d8d8939
     1.1 --- a/bin/isabelle-process	Sat May 11 18:16:17 2013 +0200
     1.2 +++ b/bin/isabelle-process	Sat May 11 18:45:38 2013 +0200
     1.3 @@ -31,7 +31,6 @@
     1.4    echo "    -S           secure mode -- disallow critical operations"
     1.5    echo "    -T ADDR      startup process wrapper, with socket address"
     1.6    echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
     1.7 -  echo "    -X           startup PGIP interaction mode"
     1.8    echo "    -e MLTEXT    pass MLTEXT to the ML session"
     1.9    echo "    -f           pass 'Session.finish();' to the ML session"
    1.10    echo "    -m MODE      add print mode for output"
    1.11 @@ -64,14 +63,13 @@
    1.12  SECURE=""
    1.13  WRAPPER_SOCKET=""
    1.14  WRAPPER_FIFOS=""
    1.15 -PGIP=""
    1.16  MLTEXT=""
    1.17  MODES=""
    1.18  TERMINATE=""
    1.19  READONLY=""
    1.20  NOWRITE=""
    1.21  
    1.22 -while getopts "IPST:W:Xe:fm:qruw" OPT
    1.23 +while getopts "IPST:W:e:fm:qruw" OPT
    1.24  do
    1.25    case "$OPT" in
    1.26      I)
    1.27 @@ -89,9 +87,6 @@
    1.28      W)
    1.29        WRAPPER_FIFOS="$OPTARG"
    1.30        ;;
    1.31 -    X)
    1.32 -      PGIP=true
    1.33 -      ;;
    1.34      e)
    1.35        MLTEXT="$MLTEXT $OPTARG"
    1.36        ;;
    1.37 @@ -226,8 +221,6 @@
    1.38    [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
    1.39    [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
    1.40    MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
    1.41 -elif [ -n "$PGIP" ]; then
    1.42 -  MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
    1.43  elif [ -n "$PROOFGENERAL" ]; then
    1.44    MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
    1.45  elif [ "$ISAR" = true ]; then