bin/isabelle
changeset 10905 e23abeef8150
parent 10585 58a1ed1edb65
child 11550 915c5de6480f
equal deleted inserted replaced
10904:624077d5afdd 10905:e23abeef8150
    27   echo "    -C           tell ML system to copy output image"
    27   echo "    -C           tell ML system to copy output image"
    28   echo "    -I           startup Isar interaction mode"
    28   echo "    -I           startup Isar interaction mode"
    29   echo "    -P           startup Proof General interaction mode"
    29   echo "    -P           startup Proof General interaction mode"
    30   echo "    -c           tell ML system to compress output image"
    30   echo "    -c           tell ML system to compress output image"
    31   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    31   echo "    -e MLTEXT    pass MLTEXT to the ML session"
       
    32   echo "    -f           pass 'Session.finish();' to the ML session"
    32   echo "    -m MODE      add print mode for output"
    33   echo "    -m MODE      add print mode for output"
    33   echo "    -q           non-interactive session"
    34   echo "    -q           non-interactive session"
    34   echo "    -r           open heap file read-only"
    35   echo "    -r           open heap file read-only"
    35   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    36   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    36   echo "    -w           reset write permissions on OUTPUT"
    37   echo "    -w           reset write permissions on OUTPUT"
    62 MODES=""
    63 MODES=""
    63 TERMINATE=""
    64 TERMINATE=""
    64 READONLY=""
    65 READONLY=""
    65 NOWRITE=""
    66 NOWRITE=""
    66 
    67 
    67 while getopts "CIPce:m:qruw" OPT
    68 while getopts "CIPce:fm:qruw" OPT
    68 do
    69 do
    69   case "$OPT" in
    70   case "$OPT" in
    70     C)
    71     C)
    71       COPYDB=true
    72       COPYDB=true
    72       ;;
    73       ;;
    79     c)
    80     c)
    80       COMPRESS=true
    81       COMPRESS=true
    81       ;;
    82       ;;
    82     e)
    83     e)
    83       MLTEXT="$MLTEXT $OPTARG"
    84       MLTEXT="$MLTEXT $OPTARG"
       
    85       ;;
       
    86     f)
       
    87       MLTEXT="$MLTEXT Session.finish();"
    84       ;;
    88       ;;
    85     m)
    89     m)
    86       if [ -z "$MODES" ]; then
    90       if [ -z "$MODES" ]; then
    87         MODES="\"$OPTARG\""
    91         MODES="\"$OPTARG\""
    88       else
    92       else