change IFS only locally -- thanks to bash arrays;
authorwenzelm
Tue Aug 04 15:05:34 2009 +0200 (2009-08-04)
changeset 3232245cb4a86eca2
parent 32321 13920dbe4547
child 32323 8185d3bfcbf1
change IFS only locally -- thanks to bash arrays;
bin/isabelle
bin/isabelle-process
lib/Tools/doc
lib/Tools/document
lib/Tools/findlogics
     1.1 --- a/bin/isabelle	Tue Aug 04 13:35:33 2009 +0200
     1.2 +++ b/bin/isabelle	Tue Aug 04 15:05:34 2009 +0200
     1.3 @@ -17,6 +17,8 @@
     1.4  ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
     1.5  source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
     1.6  
     1.7 +ORIG_IFS="$IFS"; IFS=":"; declare -a TOOLS=($ISABELLE_TOOLS); IFS="$ORIG_IFS"
     1.8 +
     1.9  
    1.10  ## diagnostics
    1.11  
    1.12 @@ -28,24 +30,19 @@
    1.13    echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
    1.14    echo
    1.15    echo "  Available tools are:"
    1.16 -  (
    1.17 -    ORIG_IFS="$IFS"
    1.18 -    IFS=":"
    1.19 -    for DIR in $ISABELLE_TOOLS
    1.20 -    do
    1.21 -      if [ -d "$DIR" ]; then
    1.22 -        cd "$DIR"
    1.23 -        for T in *
    1.24 -        do
    1.25 -          if [ -f "$T" -a -x "$T" ]; then
    1.26 -            DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
    1.27 -            echo "    $T - $DESCRLINE"
    1.28 -          fi
    1.29 -        done
    1.30 -      fi
    1.31 -    done
    1.32 -    IFS="$ORIG_IFS"
    1.33 -  )
    1.34 +  for DIR in ${TOOLS[@]}
    1.35 +  do
    1.36 +    if [ -d "$DIR" ]; then
    1.37 +      for TOOL in "$DIR"/*
    1.38 +      do
    1.39 +        if [ -f "$TOOL" -a -x "$TOOL" ]; then
    1.40 +          NAME="$(basename "$TOOL")"
    1.41 +          DESCRLINE="$(fgrep DESCRIPTION: "$TOOL" | sed -e 's/^.*DESCRIPTION: *//')"
    1.42 +          echo "    $NAME - $DESCRLINE"
    1.43 +        fi
    1.44 +      done
    1.45 +    fi
    1.46 +  done
    1.47    exit 1
    1.48  }
    1.49  
    1.50 @@ -66,13 +63,10 @@
    1.51  
    1.52  ## main
    1.53  
    1.54 -ORIG_IFS="$IFS"
    1.55 -IFS=":"
    1.56 -for DIR in $ISABELLE_TOOLS
    1.57 +for DIR in "${TOOLS[@]}"
    1.58  do
    1.59    TOOL="$DIR/$TOOLNAME"
    1.60    [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    1.61  done
    1.62 -IFS="$ORIG_IFS"
    1.63  
    1.64  fail "Unknown Isabelle tool: $TOOLNAME"
     2.1 --- a/bin/isabelle-process	Tue Aug 04 13:35:33 2009 +0200
     2.2 +++ b/bin/isabelle-process	Tue Aug 04 15:05:34 2009 +0200
     2.3 @@ -160,15 +160,13 @@
     2.4      INFILE=""
     2.5      ISA_PATH=""
     2.6  
     2.7 -    ORIG_IFS="$IFS"
     2.8 -    IFS=":"
     2.9 -    for DIR in $ISABELLE_PATH
    2.10 +    ORIG_IFS="$IFS"; IFS=":"; declare -a PATHS=($ISABELLE_PATH); IFS="$ORIG_IFS"
    2.11 +    for DIR in "${PATHS[@]}"
    2.12      do
    2.13        DIR="$DIR/$ML_IDENTIFIER"
    2.14        ISA_PATH="$ISA_PATH  $DIR\n"
    2.15        [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
    2.16      done
    2.17 -    IFS="$ORIG_IFS"
    2.18  
    2.19      if [ -z "$INFILE" ]; then
    2.20        echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
     3.1 --- a/lib/Tools/doc	Tue Aug 04 13:35:33 2009 +0200
     3.2 +++ b/lib/Tools/doc	Tue Aug 04 15:05:34 2009 +0200
     3.3 @@ -34,28 +34,23 @@
     3.4  
     3.5  ## main
     3.6  
     3.7 +ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
     3.8 +
     3.9  if [ -z "$DOC" ]; then
    3.10 -  ORIG_IFS="$IFS"
    3.11 -  IFS=":"
    3.12 -  for DIR in $ISABELLE_DOCS
    3.13 +  for DIR in "${DOCS[@]}"
    3.14    do
    3.15      [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    3.16      [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
    3.17    done
    3.18 -  IFS="$ORIG_IFS"
    3.19  else
    3.20 -  ORIG_IFS="$IFS"
    3.21 -  IFS=":"
    3.22 -  for DIR in $ISABELLE_DOCS
    3.23 +  for DIR in "${DOCS[@]}"
    3.24    do
    3.25 -    IFS="$ORIG_IFS"
    3.26      [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    3.27      for FMT in "$ISABELLE_DOC_FORMAT" dvi
    3.28      do
    3.29        [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
    3.30      done
    3.31    done
    3.32 -  IFS="$ORIG_IFS"
    3.33    fail "Unknown Isabelle document: $DOC"  
    3.34  fi
    3.35  
     4.1 --- a/lib/Tools/document	Tue Aug 04 13:35:33 2009 +0200
     4.2 +++ b/lib/Tools/document	Tue Aug 04 15:05:34 2009 +0200
     4.3 @@ -38,7 +38,7 @@
     4.4  CLEAN=""
     4.5  NAME="document"
     4.6  OUTFORMAT=dvi
     4.7 -TAGS=""
     4.8 +declare -a TAGS=()
     4.9  
    4.10  while getopts "cn:o:t:" OPT
    4.11  do
    4.12 @@ -53,7 +53,7 @@
    4.13        OUTFORMAT="$OPTARG"
    4.14        ;;
    4.15      t)
    4.16 -      TAGS="$OPTARG"
    4.17 +      ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS"
    4.18        ;;
    4.19      \?)
    4.20        usage
    4.21 @@ -90,21 +90,20 @@
    4.22  function prep_tags ()
    4.23  {
    4.24    (
    4.25 -    IFS=","
    4.26 -    for TAG in $TAGS
    4.27 +    for TAG in "${TAGS[@]}"
    4.28      do
    4.29        case "$TAG" in
    4.30          /*)
    4.31 -  	  echo "\\isafoldtag{${TAG:1}}"
    4.32 +          echo "\\isafoldtag{${TAG:1}}"
    4.33            ;;
    4.34          -*)
    4.35 -  	  echo "\\isadroptag{${TAG:1}}"
    4.36 +          echo "\\isadroptag{${TAG:1}}"
    4.37            ;;
    4.38          +*)
    4.39 -  	  echo "\\isakeeptag{${TAG:1}}"
    4.40 +          echo "\\isakeeptag{${TAG:1}}"
    4.41            ;;
    4.42          *)
    4.43 -  	  echo "\\isakeeptag{${TAG}}"
    4.44 +          echo "\\isakeeptag{${TAG}}"
    4.45            ;;
    4.46        esac
    4.47      done
     5.1 --- a/lib/Tools/findlogics	Tue Aug 04 13:35:33 2009 +0200
     5.2 +++ b/lib/Tools/findlogics	Tue Aug 04 15:05:34 2009 +0200
     5.3 @@ -22,22 +22,21 @@
     5.4  
     5.5  [ "$#" -ne 0 ] && usage
     5.6  
     5.7 -
     5.8 -LOGICS=""
     5.9 +declare -a LOGICS=()
    5.10 +declare -a ISABELLE_PATHS=()
    5.11  
    5.12 -ORIG_IFS="$IFS"
    5.13 -IFS=":"
    5.14 -for DIR in $ISABELLE_PATH
    5.15 +ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS
    5.16 +
    5.17 +for DIR in "${ISABELLE_PATHS[@]}"
    5.18  do
    5.19    DIR="$DIR/$ML_IDENTIFIER"
    5.20    for FILE in "$DIR"/*
    5.21    do
    5.22      if [ -f "$FILE" ]; then
    5.23        NAME=$(basename "$FILE")
    5.24 -      LOGICS="$LOGICS $NAME"
    5.25 +      LOGICS+=("$NAME")
    5.26      fi
    5.27    done
    5.28  done
    5.29 -IFS="$ORIG_IFS"
    5.30  
    5.31 -echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)
    5.32 +echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq)