lib/Tools/doc
changeset 15703 727ef1b8b3ee
parent 14981 e73f8140af78
child 15717 541e50adfc73
equal deleted inserted replaced
15702:2677db44c795 15703:727ef1b8b3ee
    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