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