lib/Tools/doc
changeset 32322 45cb4a86eca2
parent 29143 72c960b2b83e
child 32390 468eff174a77
     1.1 --- a/lib/Tools/doc	Tue Aug 04 13:35:33 2009 +0200
     1.2 +++ b/lib/Tools/doc	Tue Aug 04 15:05:34 2009 +0200
     1.3 @@ -34,28 +34,23 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 +ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
     1.8 +
     1.9  if [ -z "$DOC" ]; then
    1.10 -  ORIG_IFS="$IFS"
    1.11 -  IFS=":"
    1.12 -  for DIR in $ISABELLE_DOCS
    1.13 +  for DIR in "${DOCS[@]}"
    1.14    do
    1.15      [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    1.16      [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
    1.17    done
    1.18 -  IFS="$ORIG_IFS"
    1.19  else
    1.20 -  ORIG_IFS="$IFS"
    1.21 -  IFS=":"
    1.22 -  for DIR in $ISABELLE_DOCS
    1.23 +  for DIR in "${DOCS[@]}"
    1.24    do
    1.25 -    IFS="$ORIG_IFS"
    1.26      [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    1.27      for FMT in "$ISABELLE_DOC_FORMAT" dvi
    1.28      do
    1.29        [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
    1.30      done
    1.31    done
    1.32 -  IFS="$ORIG_IFS"
    1.33    fail "Unknown Isabelle document: $DOC"  
    1.34  fi
    1.35