lib/Tools/doc
changeset 2332 ae592411c199
child 2916 d761a62da697
equal deleted inserted replaced
2331:d6a56ff0d94e 2332:ae592411c199
       
     1 #!/bin/bash -norc
       
     2 #
       
     3 # $Id$
       
     4 #
       
     5 # DESCRIPTION: view Isabelle documentation
       
     6 #
       
     7 # TODO:
       
     8 #  - other formats than dvi (??)
       
     9 
       
    10 
       
    11 PRG=$(basename $0)
       
    12 
       
    13 function usage()
       
    14 {
       
    15   echo
       
    16   echo "Usage: $PRG [DOC]"
       
    17   echo
       
    18   echo "  View Isabelle documentation DOC, or show list of available documents."
       
    19   echo
       
    20   exit 1
       
    21 }
       
    22 
       
    23 function fail()
       
    24 {
       
    25   echo "$1" >&2
       
    26   exit 2
       
    27 }
       
    28 
       
    29 
       
    30 ## args
       
    31 
       
    32 DOC=""
       
    33 [ $# -ge 1 ] && { DOC="$1"; shift }
       
    34 
       
    35 [ $# -ne 0 -o "$DOC" = "-?" ] && usage
       
    36 
       
    37 
       
    38 ## main
       
    39 
       
    40 if [ -z "$DOC" ]; then
       
    41   for DIR in $ISABELLE_DOCS
       
    42   do
       
    43     [ -f $DIR/Contents ] && cat $DIR/Contents
       
    44   done
       
    45 else
       
    46   for DIR in $ISABELLE_DOCS
       
    47   do
       
    48     [ -f $DIR/$DOC.dvi ] && exec $DVI_VIEWER $DIR/$DOC.dvi
       
    49   done
       
    50   fail "Unknown Isabelle document: $DOC"  
       
    51 fi