equal
deleted
inserted
replaced
32 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage |
32 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage |
33 |
33 |
34 |
34 |
35 ## main |
35 ## main |
36 |
36 |
|
37 ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS" |
|
38 |
37 if [ -z "$DOC" ]; then |
39 if [ -z "$DOC" ]; then |
38 ORIG_IFS="$IFS" |
40 for DIR in "${DOCS[@]}" |
39 IFS=":" |
|
40 for DIR in $ISABELLE_DOCS |
|
41 do |
41 do |
42 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
42 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
43 [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents" |
43 [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents" |
44 done |
44 done |
45 IFS="$ORIG_IFS" |
|
46 else |
45 else |
47 ORIG_IFS="$IFS" |
46 for DIR in "${DOCS[@]}" |
48 IFS=":" |
|
49 for DIR in $ISABELLE_DOCS |
|
50 do |
47 do |
51 IFS="$ORIG_IFS" |
|
52 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
48 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
53 for FMT in "$ISABELLE_DOC_FORMAT" dvi |
49 for FMT in "$ISABELLE_DOC_FORMAT" dvi |
54 do |
50 do |
55 [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; } |
51 [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; } |
56 done |
52 done |
57 done |
53 done |
58 IFS="$ORIG_IFS" |
|
59 fail "Unknown Isabelle document: $DOC" |
54 fail "Unknown Isabelle document: $DOC" |
60 fi |
55 fi |
61 |
56 |