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