lib/Tools/doc
author wenzelm
Mon Dec 09 09:02:15 1996 +0100 (1996-12-09)
changeset 2332 ae592411c199
child 2916 d761a62da697
permissions -rwxr-xr-x
doc: view Isabelle documentation;
     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