# HG changeset patch
# User wenzelm
# Date 1249391134 -7200
# Node ID 45cb4a86eca2d4eec2bc52c5bcd13dd2331d8076
# Parent  13920dbe4547551e1418957b63664c6253d948b7
change IFS only locally -- thanks to bash arrays;

diff -r 13920dbe4547 -r 45cb4a86eca2 bin/isabelle
--- a/bin/isabelle	Tue Aug 04 13:35:33 2009 +0200
+++ b/bin/isabelle	Tue Aug 04 15:05:34 2009 +0200
@@ -17,6 +17,8 @@
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
+ORIG_IFS="$IFS"; IFS=":"; declare -a TOOLS=($ISABELLE_TOOLS); IFS="$ORIG_IFS"
+
 
 ## diagnostics
 
@@ -28,24 +30,19 @@
   echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
   echo
   echo "  Available tools are:"
-  (
-    ORIG_IFS="$IFS"
-    IFS=":"
-    for DIR in $ISABELLE_TOOLS
-    do
-      if [ -d "$DIR" ]; then
-        cd "$DIR"
-        for T in *
-        do
-          if [ -f "$T" -a -x "$T" ]; then
-            DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
-            echo "    $T - $DESCRLINE"
-          fi
-        done
-      fi
-    done
-    IFS="$ORIG_IFS"
-  )
+  for DIR in ${TOOLS[@]}
+  do
+    if [ -d "$DIR" ]; then
+      for TOOL in "$DIR"/*
+      do
+        if [ -f "$TOOL" -a -x "$TOOL" ]; then
+          NAME="$(basename "$TOOL")"
+          DESCRLINE="$(fgrep DESCRIPTION: "$TOOL" | sed -e 's/^.*DESCRIPTION: *//')"
+          echo "    $NAME - $DESCRLINE"
+        fi
+      done
+    fi
+  done
   exit 1
 }
 
@@ -66,13 +63,10 @@
 
 ## main
 
-ORIG_IFS="$IFS"
-IFS=":"
-for DIR in $ISABELLE_TOOLS
+for DIR in "${TOOLS[@]}"
 do
   TOOL="$DIR/$TOOLNAME"
   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
 done
-IFS="$ORIG_IFS"
 
 fail "Unknown Isabelle tool: $TOOLNAME"
diff -r 13920dbe4547 -r 45cb4a86eca2 bin/isabelle-process
--- a/bin/isabelle-process	Tue Aug 04 13:35:33 2009 +0200
+++ b/bin/isabelle-process	Tue Aug 04 15:05:34 2009 +0200
@@ -160,15 +160,13 @@
     INFILE=""
     ISA_PATH=""
 
-    ORIG_IFS="$IFS"
-    IFS=":"
-    for DIR in $ISABELLE_PATH
+    ORIG_IFS="$IFS"; IFS=":"; declare -a PATHS=($ISABELLE_PATH); IFS="$ORIG_IFS"
+    for DIR in "${PATHS[@]}"
     do
       DIR="$DIR/$ML_IDENTIFIER"
       ISA_PATH="$ISA_PATH  $DIR\n"
       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
     done
-    IFS="$ORIG_IFS"
 
     if [ -z "$INFILE" ]; then
       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
diff -r 13920dbe4547 -r 45cb4a86eca2 lib/Tools/doc
--- a/lib/Tools/doc	Tue Aug 04 13:35:33 2009 +0200
+++ b/lib/Tools/doc	Tue Aug 04 15:05:34 2009 +0200
@@ -34,28 +34,23 @@
 
 ## main
 
+ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
+
 if [ -z "$DOC" ]; then
-  ORIG_IFS="$IFS"
-  IFS=":"
-  for DIR in $ISABELLE_DOCS
+  for DIR in "${DOCS[@]}"
   do
     [ -d "$DIR" ] || fail "Bad document directory: $DIR"
     [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
   done
-  IFS="$ORIG_IFS"
 else
-  ORIG_IFS="$IFS"
-  IFS=":"
-  for DIR in $ISABELLE_DOCS
+  for DIR in "${DOCS[@]}"
   do
-    IFS="$ORIG_IFS"
     [ -d "$DIR" ] || fail "Bad document directory: $DIR"
     for FMT in "$ISABELLE_DOC_FORMAT" dvi
     do
       [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
     done
   done
-  IFS="$ORIG_IFS"
   fail "Unknown Isabelle document: $DOC"  
 fi
 
diff -r 13920dbe4547 -r 45cb4a86eca2 lib/Tools/document
--- a/lib/Tools/document	Tue Aug 04 13:35:33 2009 +0200
+++ b/lib/Tools/document	Tue Aug 04 15:05:34 2009 +0200
@@ -38,7 +38,7 @@
 CLEAN=""
 NAME="document"
 OUTFORMAT=dvi
-TAGS=""
+declare -a TAGS=()
 
 while getopts "cn:o:t:" OPT
 do
@@ -53,7 +53,7 @@
       OUTFORMAT="$OPTARG"
       ;;
     t)
-      TAGS="$OPTARG"
+      ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS"
       ;;
     \?)
       usage
@@ -90,21 +90,20 @@
 function prep_tags ()
 {
   (
-    IFS=","
-    for TAG in $TAGS
+    for TAG in "${TAGS[@]}"
     do
       case "$TAG" in
         /*)
-  	  echo "\\isafoldtag{${TAG:1}}"
+          echo "\\isafoldtag{${TAG:1}}"
           ;;
         -*)
-  	  echo "\\isadroptag{${TAG:1}}"
+          echo "\\isadroptag{${TAG:1}}"
           ;;
         +*)
-  	  echo "\\isakeeptag{${TAG:1}}"
+          echo "\\isakeeptag{${TAG:1}}"
           ;;
         *)
-  	  echo "\\isakeeptag{${TAG}}"
+          echo "\\isakeeptag{${TAG}}"
           ;;
       esac
     done
diff -r 13920dbe4547 -r 45cb4a86eca2 lib/Tools/findlogics
--- a/lib/Tools/findlogics	Tue Aug 04 13:35:33 2009 +0200
+++ b/lib/Tools/findlogics	Tue Aug 04 15:05:34 2009 +0200
@@ -22,22 +22,21 @@
 
 [ "$#" -ne 0 ] && usage
 
-
-LOGICS=""
+declare -a LOGICS=()
+declare -a ISABELLE_PATHS=()
 
-ORIG_IFS="$IFS"
-IFS=":"
-for DIR in $ISABELLE_PATH
+ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS
+
+for DIR in "${ISABELLE_PATHS[@]}"
 do
   DIR="$DIR/$ML_IDENTIFIER"
   for FILE in "$DIR"/*
   do
     if [ -f "$FILE" ]; then
       NAME=$(basename "$FILE")
-      LOGICS="$LOGICS $NAME"
+      LOGICS+=("$NAME")
     fi
   done
 done
-IFS="$ORIG_IFS"
 
-echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)
+echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq)