lib/Tools/doc
author wenzelm
Fri Apr 11 17:30:15 1997 +0200 (1997-04-11)
changeset 2936 bd33e7aae062
parent 2916 d761a62da697
child 2940 baae674b1d29
permissions -rwxr-xr-x
fixed { ... } shell syntax to accomodate bash 2.x;
     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 ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    49   done
    50   fail "Unknown Isabelle document: $DOC"  
    51 fi