equal
deleted
inserted
replaced
38 if [ -z "$DOC" ]; then |
38 if [ -z "$DOC" ]; then |
39 ORIG_IFS="$IFS" |
39 ORIG_IFS="$IFS" |
40 IFS=":" |
40 IFS=":" |
41 for DIR in $ISABELLE_DOCS |
41 for DIR in $ISABELLE_DOCS |
42 do |
42 do |
|
43 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
43 [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents" |
44 [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents" |
44 done |
45 done |
45 IFS="$ORIG_IFS" |
46 IFS="$ORIG_IFS" |
46 else |
47 else |
47 ORIG_IFS="$IFS" |
48 ORIG_IFS="$IFS" |
48 IFS=":" |
49 IFS=":" |
49 for DIR in $ISABELLE_DOCS |
50 for DIR in $ISABELLE_DOCS |
50 do |
51 do |
51 [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; } |
52 IFS="$ORIG_IFS" |
|
53 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
|
54 for FMT in "$ISABELLE_DOC_FORMAT" dvi |
|
55 do |
|
56 [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; } |
|
57 done |
52 done |
58 done |
53 IFS="$ORIG_IFS" |
59 IFS="$ORIG_IFS" |
54 fail "Unknown Isabelle document: $DOC" |
60 fail "Unknown Isabelle document: $DOC" |
55 fi |
61 fi |