bin/isabelle
changeset 2292 c1c5652600f1
child 2308 641be5ad47af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/bin/isabelle	Mon Dec 02 18:13:28 1996 +0100
     1.3 @@ -0,0 +1,162 @@
     1.4 +#!/bin/bash
     1.5 +#
     1.6 +# Basic Isabelle startup script.
     1.7 +#
     1.8 +# $Id$
     1.9 +
    1.10 +
    1.11 +## settings
    1.12 +
    1.13 +ISABELLE_HOME=$(dirname $(dirname $0))
    1.14 +. $ISABELLE_HOME/lib/scripts/getsettings
    1.15 +
    1.16 +#get bash-style platform info
    1.17 +unset HOSTTYPE
    1.18 +unset OSTYPE
    1.19 +PLATFORM=$(bash -noprofile -c 'echo $HOSTTYPE-$OSTYPE')
    1.20 +
    1.21 +
    1.22 +## diagnostics
    1.23 +
    1.24 +PRG=$(basename $0)
    1.25 +
    1.26 +function usage()
    1.27 +{
    1.28 +  echo
    1.29 +  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    1.30 +  echo
    1.31 +  echo "  Options are:"
    1.32 +  echo "    -c           force copying of heap file"
    1.33 +  echo "    -e MLTEXT    pass MLTEXT to ML session"
    1.34 +#FIXME  echo "    -o OPTIONS   pass options to ML system"
    1.35 +  echo "    -q           non-interactive session"
    1.36 +  echo "    -r           open heap file read-only"
    1.37 +  echo "    -u           pass 'use\"ROOT.ML\" handle _ => exit 1; commit();'"
    1.38 +  echo "                 to the ML session"
    1.39 +  echo
    1.40 +  echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    1.41 +  echo "  These are either names to be searched in the Isabelle path, or actual"
    1.42 +  echo "  file names (containing at least one /)."
    1.43 +  echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
    1.44 +  echo
    1.45 +  exit 1
    1.46 +}
    1.47 +
    1.48 +function fail()
    1.49 +{
    1.50 +  echo "$1"
    1.51 +  exit 2
    1.52 +}
    1.53 +
    1.54 +
    1.55 +## process command line
    1.56 +
    1.57 +# options
    1.58 +
    1.59 +COPYDB=""
    1.60 +MLTEXT=""
    1.61 +COPYDB=""
    1.62 +OPTIONS=""
    1.63 +TERMINATE=""
    1.64 +READONLY=""
    1.65 +
    1.66 +while getopts "ce:qru" OPT
    1.67 +do
    1.68 +  case "$OPT" in
    1.69 +    c)
    1.70 +      COPYDB=true
    1.71 +      ;;
    1.72 +    e)
    1.73 +      MLTEXT="$MLTEXT $OPTARG"
    1.74 +      ;;
    1.75 +    o)
    1.76 +      OPTIONS="$OPTIONS $OPTARG"
    1.77 +      ;;
    1.78 +    q)
    1.79 +      TERMINATE=true
    1.80 +      ;;
    1.81 +    r)
    1.82 +      READONLY=true
    1.83 +      ;;
    1.84 +    u)
    1.85 +      MLTEXT="$MLTEXT use\"ROOT.ML\" handle _ => exit 1; commit();"
    1.86 +      ;;
    1.87 +    \?)
    1.88 +      usage
    1.89 +      ;;
    1.90 +  esac
    1.91 +done
    1.92 +
    1.93 +shift $(($OPTIND - 1))
    1.94 +
    1.95 +
    1.96 +# args
    1.97 +
    1.98 +INPUT=""
    1.99 +OUTPUT=""
   1.100 +
   1.101 +if [ $# -ge 1 ]; then
   1.102 +  INPUT="$1"
   1.103 +  shift
   1.104 +fi
   1.105 +
   1.106 +if [ $# -ge 1 ]; then
   1.107 +  OUTPUT="$1"
   1.108 +  shift
   1.109 +fi
   1.110 +
   1.111 +[ $# -ne 0 ] && fail "Bad args: $*"
   1.112 +
   1.113 +
   1.114 +## check ML system
   1.115 +
   1.116 +[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Sorry, no Isabelle."
   1.117 +
   1.118 +
   1.119 +## input heap file
   1.120 +
   1.121 +[ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
   1.122 +
   1.123 +case "$INPUT" in
   1.124 +  SYSTEM)
   1.125 +    INFILE=""
   1.126 +    ;;
   1.127 +  */*)
   1.128 +    INFILE="$INPUT"
   1.129 +    [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
   1.130 +    ;;
   1.131 +  *)
   1.132 +    INFILE=""
   1.133 +    for DIR in $(echo $ISABELLE_PATH | tr : " ")
   1.134 +    do
   1.135 +      [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   1.136 +    done
   1.137 +    [ -z "$INFILE" ] && fail "Unknown logic: \"$INPUT\""
   1.138 +    ;;
   1.139 +esac
   1.140 +
   1.141 +
   1.142 +## output heap file
   1.143 +
   1.144 +case "$OUTPUT" in
   1.145 +  "")
   1.146 +    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   1.147 +    ;;
   1.148 +  */*)
   1.149 +    OUTFILE="$OUTPUT"
   1.150 +    ;;
   1.151 +  *)
   1.152 +    OUTDIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
   1.153 +    mkdir -p "$OUTDIR"
   1.154 +    OUTFILE="$OUTDIR/$OUTPUT"
   1.155 +    ;;
   1.156 +esac
   1.157 +
   1.158 +
   1.159 +## run it!
   1.160 +
   1.161 +ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   1.162 +
   1.163 +export INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE
   1.164 +[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   1.165 +exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE