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