bin/isabelle
changeset 9786 270ca580b880
parent 8359 124ad46105dd
child 9972 05afcc505da3
     1.1 --- a/bin/isabelle	Fri Sep 01 17:45:07 2000 +0200
     1.2 +++ b/bin/isabelle	Fri Sep 01 17:47:20 2000 +0200
     1.3 @@ -1,16 +1,18 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # Basic Isabelle startup script.
    1.11  
    1.12  
    1.13  ## settings
    1.14  
    1.15 -PRG=$(basename $0)
    1.16 +PRG=$(basename "$0")
    1.17  
    1.18 -ISABELLE_HOME=$(dirname $0)/..
    1.19 -. $ISABELLE_HOME/lib/scripts/getsettings || \
    1.20 +ISABELLE_HOME=$(dirname "$0")/..
    1.21 +. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    1.22    { echo "$PRG probably not called from its original place!"; exit 2; }
    1.23  
    1.24  
    1.25 @@ -102,17 +104,17 @@
    1.26  INPUT=""
    1.27  OUTPUT=""
    1.28  
    1.29 -if [ $# -ge 1 ]; then
    1.30 +if [ "$#" -ge 1 ]; then
    1.31    INPUT="$1"
    1.32    shift
    1.33  fi
    1.34  
    1.35 -if [ $# -ge 1 ]; then
    1.36 +if [ "$#" -ge 1 ]; then
    1.37    OUTPUT="$1"
    1.38    shift
    1.39  fi
    1.40  
    1.41 -[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
    1.42 +[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
    1.43  
    1.44  
    1.45  ## check ML system
    1.46 @@ -133,19 +135,22 @@
    1.47      [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
    1.48      ;;
    1.49    *)
    1.50 +    INFILE=""
    1.51      ISA_PATH=""
    1.52 -    INFILE=""
    1.53 -    for DIR in $(echo $ISABELLE_PATH | tr : " ")
    1.54 +
    1.55 +    ORIG_IFS="$IFS"
    1.56 +    IFS=":"
    1.57 +    for DIR in $ISABELLE_PATH
    1.58      do
    1.59 -      ISA_PATH="$ISA_PATH $DIR"
    1.60 -      [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT
    1.61 +      DIR="$DIR/$ML_IDENTIFIER"
    1.62 +      ISA_PATH="$ISA_PATH  $DIR\n"
    1.63 +      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
    1.64      done
    1.65 +    IFS="$ORIG_IFS"
    1.66 +
    1.67      if [ -z "$INFILE" ]; then
    1.68        echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
    1.69 -      for DIR in $ISA_PATH
    1.70 -      do
    1.71 -        echo "  $DIR" >&2
    1.72 -      done
    1.73 +      echo -ne "$ISA_PATH" >&2
    1.74        exit 2
    1.75      fi
    1.76      ;;
    1.77 @@ -178,20 +183,20 @@
    1.78  
    1.79  ## run it!
    1.80  
    1.81 -ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    1.82 +ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
    1.83  
    1.84  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.85  
    1.86  export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
    1.87  
    1.88 -if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
    1.89 -  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
    1.90 +if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
    1.91 +  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
    1.92  else
    1.93 -  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
    1.94 +  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
    1.95  fi
    1.96 -RC=$?
    1.97 +RC="$?"
    1.98  
    1.99  #Do not even think of 'rm -r'!!
   1.100 -rmdir $ISABELLE_TMP
   1.101 +rmdir "$ISABELLE_TMP"
   1.102  
   1.103 -exit $RC
   1.104 +exit "$RC"