bin/isabelle
changeset 2704 afa01c9f1ab0
parent 2591 ae16f162f973
child 2711 098f9ce0541a
equal deleted inserted replaced
2703:5ce1310560ff 2704:afa01c9f1ab0
     5 # Basic Isabelle startup script.
     5 # Basic Isabelle startup script.
     6 
     6 
     7 
     7 
     8 ## settings
     8 ## settings
     9 
     9 
       
    10 PRG=$(basename $0)
       
    11 
    10 ISABELLE_HOME=$(dirname $(dirname $0))
    12 ISABELLE_HOME=$(dirname $(dirname $0))
    11 . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
    13 case "$ISABELLE_HOME" in
       
    14   /*)
       
    15     if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
       
    16       . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
       
    17     else
       
    18       echo "ERROR: $PRG probably not called from its original place!"
       
    19       exit 1
       
    20     fi
       
    21     ;;
       
    22   *)
       
    23     echo "ERROR: $PRG not called with absolute path specification!"
       
    24     exit 1
       
    25     ;;
       
    26 esac
    12 
    27 
    13 
    28 
    14 ## diagnostics
    29 ## diagnostics
    15 
       
    16 PRG=$(basename $0)
       
    17 
    30 
    18 function usage()
    31 function usage()
    19 {
    32 {
    20   echo
    33   echo
    21   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    34   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    22   echo
    35   echo
    23   echo "  Options are:"
    36   echo "  Options are:"
    24   echo "    -c           force copying of heap file (for Poly/ML)"
    37   echo "    -c           force copying of heap file (for Poly/ML)"
    25   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    38   echo "    -e MLTEXT    pass MLTEXT to the ML session"
       
    39   echo "    -m MODE      add print mode for output"
    26   echo "    -q           non-interactive session"
    40   echo "    -q           non-interactive session"
    27   echo "    -r           open heap file read-only"
    41   echo "    -r           open heap file read-only"
    28   echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
    42   echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
    29   echo
    43   echo
    30   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    44   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    47 # options
    61 # options
    48 
    62 
    49 COPYDB=""
    63 COPYDB=""
    50 MLTEXT=""
    64 MLTEXT=""
    51 COPYDB=""
    65 COPYDB=""
       
    66 MODES=""
    52 TERMINATE=""
    67 TERMINATE=""
    53 READONLY=""
    68 READONLY=""
    54 
    69 
    55 while getopts "ce:qru" OPT
    70 while getopts "ce:m:qru" OPT
    56 do
    71 do
    57   case "$OPT" in
    72   case "$OPT" in
    58     c)
    73     c)
    59       COPYDB=true
    74       COPYDB=true
    60       ;;
    75       ;;
    61     e)
    76     e)
    62       MLTEXT="$MLTEXT $OPTARG"
    77       MLTEXT="$MLTEXT $OPTARG"
       
    78       ;;
       
    79     m)
       
    80       if [ -z "$MODES" ]; then
       
    81         MODES="\"$OPTARG\""
       
    82       else
       
    83         MODES="$MODES, \"$OPTARG\""
       
    84       fi
    63       ;;
    85       ;;
    64     q)
    86     q)
    65       TERMINATE=true
    87       TERMINATE=true
    66       ;;
    88       ;;
    67     r)
    89     r)
   153 
   175 
   154 ## run it!
   176 ## run it!
   155 
   177 
   156 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   178 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   157 
   179 
       
   180 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
       
   181 
   158 export INFILE OUTFILE COPYDB MLTEXT TERMINATE
   182 export INFILE OUTFILE COPYDB MLTEXT TERMINATE
   159 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   183 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   160 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   184 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE