GPLed;
authorwenzelm
Fri Sep 01 17:47:20 2000 +0200 (2000-09-01)
changeset 9786270ca580b880
parent 9785 1634fdb11b00
child 9787 fb8c5a66dbe8
GPLed;
more robust handling of spaces in args / file names;
tuned;
bin/isabelle
bin/isatool
     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"
     2.1 --- a/bin/isatool	Fri Sep 01 17:45:07 2000 +0200
     2.2 +++ b/bin/isatool	Fri Sep 01 17:47:20 2000 +0200
     2.3 @@ -1,24 +1,24 @@
     2.4  #!/bin/bash
     2.5  #
     2.6  # $Id$
     2.7 +# Author: Markus Wenzel, TU Muenchen
     2.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.9  #
    2.10 -# Isabelle tool starter -- provides settings environment,
    2.11 -#   and keeps your PATH name space clean.
    2.12 +# Isabelle tool starter -- provides settings environment
    2.13 +# and keeps your PATH name space clean.
    2.14  
    2.15  
    2.16  ## settings
    2.17  
    2.18 -PRG=$(basename $0)
    2.19 +PRG=$(basename "$0")
    2.20  
    2.21 -ISABELLE_HOME=$(dirname $0)/..
    2.22 -. $ISABELLE_HOME/lib/scripts/getsettings || \
    2.23 +ISABELLE_HOME=$(dirname "$0")/..
    2.24 +. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    2.25    { echo "$PRG probably not called from its original place!"; exit 2; }
    2.26  
    2.27  
    2.28  ## diagnostics
    2.29  
    2.30 -TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
    2.31 -
    2.32  function usage()
    2.33  {
    2.34    echo
    2.35 @@ -29,9 +29,11 @@
    2.36    echo
    2.37    echo "  Available tools are:"
    2.38    (
    2.39 -    for DIR in $TOOLDIRS
    2.40 +    ORIG_IFS="$IFS"
    2.41 +    IFS=":"
    2.42 +    for DIR in $ISABELLE_TOOLS
    2.43      do
    2.44 -      cd $DIR
    2.45 +      cd "$DIR"
    2.46        echo
    2.47        for T in *
    2.48        do
    2.49 @@ -41,6 +43,7 @@
    2.50          fi
    2.51        done
    2.52      done
    2.53 +    IFS="$ORIG_IFS"
    2.54    )
    2.55    echo
    2.56    exit 1
    2.57 @@ -55,7 +58,7 @@
    2.58  
    2.59  ## args
    2.60  
    2.61 -[ $# -lt 1 -o "$1" = "-?" ] && usage
    2.62 +[ "$#" -lt 1 -o "$1" = "-?" ] && usage
    2.63  
    2.64  TOOLNAME="$1"
    2.65  shift
    2.66 @@ -63,10 +66,13 @@
    2.67  
    2.68  ## main
    2.69  
    2.70 -for DIR in $TOOLDIRS
    2.71 +ORIG_IFS="$IFS"
    2.72 +IFS=":"
    2.73 +for DIR in $ISABELLE_TOOLS
    2.74  do
    2.75 -  TOOL=$DIR/$TOOLNAME
    2.76 +  TOOL="$DIR/$TOOLNAME"
    2.77    [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    2.78  done
    2.79 +IFS="$ORIG_IFS"
    2.80  
    2.81  fail "Unknown Isabelle tool: $TOOLNAME"