bin/isabelle
author wenzelm
Fri Feb 28 16:56:31 1997 +0100 (1997-02-28)
changeset 2704 afa01c9f1ab0
parent 2591 ae16f162f973
child 2711 098f9ce0541a
permissions -rwxr-xr-x
more robust handling of invocation errors;
added -m MODE option;
     1 #!/bin/bash -norc
     2 #
     3 # $Id$
     4 #
     5 # Basic Isabelle startup script.
     6 
     7 
     8 ## settings
     9 
    10 PRG=$(basename $0)
    11 
    12 ISABELLE_HOME=$(dirname $(dirname $0))
    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
    27 
    28 
    29 ## diagnostics
    30 
    31 function usage()
    32 {
    33   echo
    34   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    35   echo
    36   echo "  Options are:"
    37   echo "    -c           force copying of heap file (for Poly/ML)"
    38   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    39   echo "    -m MODE      add print mode for output"
    40   echo "    -q           non-interactive session"
    41   echo "    -r           open heap file read-only"
    42   echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
    43   echo
    44   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    45   echo "  These are either names to be searched in the Isabelle path, or actual"
    46   echo "  file names (then containing at least one /)."
    47   echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
    48   echo
    49   exit 1
    50 }
    51 
    52 function fail()
    53 {
    54   echo "$1" >&2
    55   exit 2
    56 }
    57 
    58 
    59 ## process command line
    60 
    61 # options
    62 
    63 COPYDB=""
    64 MLTEXT=""
    65 COPYDB=""
    66 MODES=""
    67 TERMINATE=""
    68 READONLY=""
    69 
    70 while getopts "ce:m:qru" OPT
    71 do
    72   case "$OPT" in
    73     c)
    74       COPYDB=true
    75       ;;
    76     e)
    77       MLTEXT="$MLTEXT $OPTARG"
    78       ;;
    79     m)
    80       if [ -z "$MODES" ]; then
    81         MODES="\"$OPTARG\""
    82       else
    83         MODES="$MODES, \"$OPTARG\""
    84       fi
    85       ;;
    86     q)
    87       TERMINATE=true
    88       ;;
    89     r)
    90       READONLY=true
    91       ;;
    92     u)
    93       MLTEXT="$MLTEXT exit_use_dir\".\";"
    94       ;;
    95     \?)
    96       usage
    97       ;;
    98   esac
    99 done
   100 
   101 shift $(($OPTIND - 1))
   102 
   103 
   104 # args
   105 
   106 INPUT=""
   107 OUTPUT=""
   108 
   109 if [ $# -ge 1 ]; then
   110   INPUT="$1"
   111   shift
   112 fi
   113 
   114 if [ $# -ge 1 ]; then
   115   OUTPUT="$1"
   116   shift
   117 fi
   118 
   119 [ $# -ne 0 ] && { echo "Bad args: $*"; usage }
   120 
   121 
   122 ## check ML system
   123 
   124 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   125 
   126 
   127 ## input heap file
   128 
   129 [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
   130 
   131 case "$INPUT" in
   132   SYSTEM)
   133     INFILE=""
   134     ;;
   135   */*)
   136     INFILE="$INPUT"
   137     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   138     ;;
   139   *)
   140     ISA_PATH=""
   141     INFILE=""
   142     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   143     do
   144       ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"
   145       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   146     done
   147     if [ -z "$INFILE" ]; then
   148       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   149       for DIR in $ISA_PATH
   150       do
   151         echo "  $DIR" >&2
   152       done
   153       exit 2
   154     fi
   155     ;;
   156 esac
   157 
   158 
   159 ## output heap file
   160 
   161 case "$OUTPUT" in
   162   "")
   163     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   164     ;;
   165   */*)
   166     OUTFILE="$OUTPUT"
   167     ;;
   168   *)
   169     OUTDIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
   170     mkdir -p "$OUTDIR"
   171     OUTFILE="$OUTDIR/$OUTPUT"
   172     ;;
   173 esac
   174 
   175 
   176 ## run it!
   177 
   178 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   179 
   180 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   181 
   182 export INFILE OUTFILE COPYDB MLTEXT TERMINATE
   183 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   184 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE