bin/isabelle
changeset 11550 915c5de6480f
parent 10905 e23abeef8150
child 11566 94d2d6531c57
     1.1 --- a/bin/isabelle	Tue Sep 04 21:10:57 2001 +0200
     1.2 +++ b/bin/isabelle	Sat Sep 08 20:00:31 2001 +0200
     1.3 @@ -4,220 +4,12 @@
     1.4  # Author: Markus Wenzel, TU Muenchen
     1.5  # License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.6  #
     1.7 -# Basic Isabelle startup script.
     1.8 -
     1.9 -
    1.10 -## settings
    1.11 -
    1.12 -PRG="$(basename "$0")"
    1.13 -
    1.14 -ISABELLE_HOME="$(dirname "$0")/.."
    1.15 -. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    1.16 -  { echo "$PRG probably not called from its original place!"; exit 2; }
    1.17 -
    1.18 -
    1.19 -## diagnostics
    1.20 -
    1.21 -function usage()
    1.22 -{
    1.23 -  echo
    1.24 -  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    1.25 -  echo
    1.26 -  echo "  Options are:"
    1.27 -  echo "    -C           tell ML system to copy output image"
    1.28 -  echo "    -I           startup Isar interaction mode"
    1.29 -  echo "    -P           startup Proof General interaction mode"
    1.30 -  echo "    -c           tell ML system to compress output image"
    1.31 -  echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.32 -  echo "    -f           pass 'Session.finish();' to the ML session"
    1.33 -  echo "    -m MODE      add print mode for output"
    1.34 -  echo "    -q           non-interactive session"
    1.35 -  echo "    -r           open heap file read-only"
    1.36 -  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    1.37 -  echo "    -w           reset write permissions on OUTPUT"
    1.38 -  echo
    1.39 -  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    1.40 -  echo "  These are either names to be searched in the Isabelle path, or"
    1.41 -  echo "  actual file names (containing at least one /)."
    1.42 -  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    1.43 -  echo
    1.44 -  exit 1
    1.45 -}
    1.46 -
    1.47 -function fail()
    1.48 -{
    1.49 -  echo "$1" >&2
    1.50 -  exit 2
    1.51 -}
    1.52 -
    1.53 -
    1.54 -## process command line
    1.55 -
    1.56 -# options
    1.57 +# Smart selection of isabelle-process versus isabelle-interface.
    1.58  
    1.59 -COPYDB=""
    1.60 -ISAR=false
    1.61 -PROOFGENERAL=""
    1.62 -COMPRESS=""
    1.63 -MLTEXT=""
    1.64 -MODES=""
    1.65 -TERMINATE=""
    1.66 -READONLY=""
    1.67 -NOWRITE=""
    1.68 -
    1.69 -while getopts "CIPce:fm:qruw" OPT
    1.70 -do
    1.71 -  case "$OPT" in
    1.72 -    C)
    1.73 -      COPYDB=true
    1.74 -      ;;
    1.75 -    I)
    1.76 -      ISAR=true
    1.77 -      ;;
    1.78 -    P)
    1.79 -      PROOFGENERAL=true
    1.80 -      ;;
    1.81 -    c)
    1.82 -      COMPRESS=true
    1.83 -      ;;
    1.84 -    e)
    1.85 -      MLTEXT="$MLTEXT $OPTARG"
    1.86 -      ;;
    1.87 -    f)
    1.88 -      MLTEXT="$MLTEXT Session.finish();"
    1.89 -      ;;
    1.90 -    m)
    1.91 -      if [ -z "$MODES" ]; then
    1.92 -        MODES="\"$OPTARG\""
    1.93 -      else
    1.94 -        MODES="\"$OPTARG\", $MODES"
    1.95 -      fi
    1.96 -      ;;
    1.97 -    q)
    1.98 -      TERMINATE=true
    1.99 -      ;;
   1.100 -    r)
   1.101 -      READONLY=true
   1.102 -      ;;
   1.103 -    u)
   1.104 -      MLTEXT="$MLTEXT use\"ROOT.ML\";"
   1.105 -      ;;
   1.106 -    w)
   1.107 -      NOWRITE=true
   1.108 -      ;;
   1.109 -    \?)
   1.110 -      usage
   1.111 -      ;;
   1.112 -  esac
   1.113 -done
   1.114 -
   1.115 -shift $(($OPTIND - 1))
   1.116 +THIS=$(cd "$(dirname "$0")"; pwd)
   1.117 +NAME="$(basename "$0")"
   1.118  
   1.119 -
   1.120 -# args
   1.121 -
   1.122 -INPUT=""
   1.123 -OUTPUT=""
   1.124 -
   1.125 -if [ "$#" -ge 1 ]; then
   1.126 -  INPUT="$1"
   1.127 -  shift
   1.128 -fi
   1.129 -
   1.130 -if [ "$#" -ge 1 ]; then
   1.131 -  OUTPUT="$1"
   1.132 -  shift
   1.133 -fi
   1.134 -
   1.135 -[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
   1.136 -
   1.137 -
   1.138 -## check ML system
   1.139 -
   1.140 -[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   1.141 -
   1.142 -
   1.143 -## input heap file
   1.144 -
   1.145 -[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   1.146 -
   1.147 -case "$INPUT" in
   1.148 -  RAW_ML_SYSTEM)
   1.149 -    INFILE=""
   1.150 -    ;;
   1.151 -  */*)
   1.152 -    INFILE="$INPUT"
   1.153 -    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   1.154 -    ;;
   1.155 -  *)
   1.156 -    INFILE=""
   1.157 -    ISA_PATH=""
   1.158 -
   1.159 -    ORIG_IFS="$IFS"
   1.160 -    IFS=":"
   1.161 -    for DIR in $ISABELLE_PATH
   1.162 -    do
   1.163 -      DIR="$DIR/$ML_IDENTIFIER"
   1.164 -      ISA_PATH="$ISA_PATH  $DIR\n"
   1.165 -      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   1.166 -    done
   1.167 -    IFS="$ORIG_IFS"
   1.168 +PRG=isabelle-interface
   1.169 +[ "$NAME" = isabelle ] && PRG=isabelle-process
   1.170  
   1.171 -    if [ -z "$INFILE" ]; then
   1.172 -      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   1.173 -      echo -ne "$ISA_PATH" >&2
   1.174 -      exit 2
   1.175 -    fi
   1.176 -    ;;
   1.177 -esac
   1.178 -
   1.179 -
   1.180 -## output heap file
   1.181 -
   1.182 -case "$OUTPUT" in
   1.183 -  "")
   1.184 -    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   1.185 -    ;;
   1.186 -  */*)
   1.187 -    OUTFILE="$OUTPUT"
   1.188 -    ;;
   1.189 -  *)
   1.190 -    mkdir -p "$ISABELLE_OUTPUT"
   1.191 -    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   1.192 -    ;;
   1.193 -esac
   1.194 -
   1.195 -
   1.196 -## prepare tmp directory
   1.197 -
   1.198 -[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   1.199 -
   1.200 -ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   1.201 -mkdir -p "$ISABELLE_TMP"
   1.202 -
   1.203 -
   1.204 -## run it!
   1.205 -
   1.206 -ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   1.207 -
   1.208 -[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   1.209 -
   1.210 -if [ -n "$PROOFGENERAL" ]; then
   1.211 -  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   1.212 -elif [ "$ISAR" = true ]; then
   1.213 -  MLTEXT="$MLTEXT; Isar.main();"
   1.214 -fi
   1.215 -
   1.216 -export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   1.217 -
   1.218 -if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   1.219 -  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   1.220 -else
   1.221 -  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   1.222 -fi
   1.223 -RC="$?"
   1.224 -
   1.225 -#Do not even think of 'rm -r'!!
   1.226 -rmdir "$ISABELLE_TMP"
   1.227 -
   1.228 -exit "$RC"
   1.229 +exec "$THIS/$PRG" "$@"