bin/isabelle-process
changeset 28043 4d05f04cc671
parent 27201 e0323036bcf2
child 28138 03e5196b1559
equal deleted inserted replaced
28042:1471f2974eb1 28043:4d05f04cc671
    30   echo "    -C           tell ML system to copy output image"
    30   echo "    -C           tell ML system to copy output image"
    31   echo "    -I           startup Isar interaction mode"
    31   echo "    -I           startup Isar interaction mode"
    32   echo "    -P           startup Proof General interaction mode"
    32   echo "    -P           startup Proof General interaction mode"
    33   echo "    -S           secure mode -- disallow critical operations"
    33   echo "    -S           secure mode -- disallow critical operations"
    34   echo "    -X           startup PGIP interaction mode"
    34   echo "    -X           startup PGIP interaction mode"
    35   echo "    -W           startup process wrapper (interaction via external program)"
    35   echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
    36   echo "    -c           tell ML system to compress output image"
    36   echo "    -c           tell ML system to compress output image"
    37   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    37   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    38   echo "    -f           pass 'Session.finish();' to the ML session"
    38   echo "    -f           pass 'Session.finish();' to the ML session"
    39   echo "    -m MODE      add print mode for output"
    39   echo "    -m MODE      add print mode for output"
    40   echo "    -q           non-interactive session"
    40   echo "    -q           non-interactive session"
    63 
    63 
    64 COPYDB=""
    64 COPYDB=""
    65 ISAR=false
    65 ISAR=false
    66 PROOFGENERAL=""
    66 PROOFGENERAL=""
    67 SECURE=""
    67 SECURE=""
    68 WRAPPER=""
    68 WRAPPER_OUTPUT=""
    69 PGIP=""
    69 PGIP=""
    70 COMPRESS=""
    70 COMPRESS=""
    71 MLTEXT=""
    71 MLTEXT=""
    72 MODES=""
    72 MODES=""
    73 TERMINATE=""
    73 TERMINATE=""
    74 READONLY=""
    74 READONLY=""
    75 NOWRITE=""
    75 NOWRITE=""
    76 
    76 
    77 while getopts "CIPSWXce:fm:qruw" OPT
    77 while getopts "CIPSW:Xce:fm:qruw" OPT
    78 do
    78 do
    79   case "$OPT" in
    79   case "$OPT" in
    80     C)
    80     C)
    81       COPYDB=true
    81       COPYDB=true
    82       ;;
    82       ;;
    88       ;;
    88       ;;
    89     S)
    89     S)
    90       SECURE=true
    90       SECURE=true
    91       ;;
    91       ;;
    92     W)
    92     W)
    93       WRAPPER=true
    93       WRAPPER_OUTPUT="$OPTARG"
    94       ;;
    94       ;;
    95     X)
    95     X)
    96       PGIP=true
    96       PGIP=true
    97       ;;
    97       ;;
    98     c)
    98     c)
   221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   222 
   222 
   223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   224 
   224 
   225 NICE="nice"
   225 NICE="nice"
   226 if [ -n "$WRAPPER" ]; then
   226 if [ -n "$WRAPPER_OUTPUT" ]; then
   227   MLTEXT="$MLTEXT; IsabelleProcess.init();"
   227   MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
   228 elif [ -n "$PGIP" ]; then
   228 elif [ -n "$PGIP" ]; then
   229   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   229   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   230 elif [ -n "$PROOFGENERAL" ]; then
   230 elif [ -n "$PROOFGENERAL" ]; then
   231   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   231   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   232 elif [ "$ISAR" = true ]; then
   232 elif [ "$ISAR" = true ]; then