bin/isabelle
changeset 10104 cf49932f3c42
parent 9982 1860276fc8de
child 10511 efb3428c9879
equal deleted inserted replaced
10103:4e446f8cef3e 10104:cf49932f3c42
    22 {
    22 {
    23   echo
    23   echo
    24   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    24   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    25   echo
    25   echo
    26   echo "  Options are:"
    26   echo "  Options are:"
       
    27   echo "    -C           tell ML system to copy output image"
    27   echo "    -I           startup Isar interaction mode"
    28   echo "    -I           startup Isar interaction mode"
    28   echo "    -P           startup Proof General interaction mode"
    29   echo "    -P           startup Proof General interaction mode"
    29   echo "    -c           tell ML system to compress output image"
    30   echo "    -c           tell ML system to compress output image"
    30   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    31   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    31   echo "    -m MODE      add print mode for output"
    32   echo "    -m MODE      add print mode for output"
    51 
    52 
    52 ## process command line
    53 ## process command line
    53 
    54 
    54 # options
    55 # options
    55 
    56 
       
    57 COPYDB=""
    56 ISAR=false
    58 ISAR=false
    57 PROOFGENERAL=""
    59 PROOFGENERAL=""
    58 COMPRESS=""
    60 COMPRESS=""
    59 MLTEXT=""
    61 MLTEXT=""
    60 MODES=""
    62 MODES=""
    61 TERMINATE=""
    63 TERMINATE=""
    62 READONLY=""
    64 READONLY=""
    63 NOWRITE=""
    65 NOWRITE=""
    64 
    66 
    65 while getopts "IPce:m:qruw" OPT
    67 while getopts "CIPce:m:qruw" OPT
    66 do
    68 do
    67   case "$OPT" in
    69   case "$OPT" in
       
    70     C)
       
    71       COPYDB=true
       
    72       ;;
    68     I)
    73     I)
    69       ISAR=true
    74       ISAR=true
    70       ;;
    75       ;;
    71     P)
    76     P)
    72       PROOFGENERAL=true
    77       PROOFGENERAL=true
   197   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   202   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   198 elif [ "$ISAR" = true ]; then
   203 elif [ "$ISAR" = true ]; then
   199   MLTEXT="$MLTEXT; Isar.main();"
   204   MLTEXT="$MLTEXT; Isar.main();"
   200 fi
   205 fi
   201 
   206 
   202 export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   207 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   203 
   208 
   204 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   209 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   205   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   210   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   206 else
   211 else
   207   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   212   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"