lib/Tools/doc
author wenzelm
Tue Apr 22 11:37:12 1997 +0200 (1997-04-22)
changeset 3007 e5efa177ee0c
parent 2940 baae674b1d29
child 3173 0013af1bc2c4
permissions -rwxr-xr-x
removed -norc;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: view Isabelle documentation
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG [DOC]"
    14   echo
    15   echo "  View Isabelle documentation DOC, or show list of available documents."
    16   echo
    17   exit 1
    18 }
    19 
    20 function fail()
    21 {
    22   echo "$1" >&2
    23   exit 2
    24 }
    25 
    26 
    27 ## args
    28 
    29 DOC=""
    30 [ $# -ge 1 ] && { DOC="$1"; shift; }
    31 
    32 [ $# -ne 0 -o "$DOC" = "-?" ] && usage
    33 
    34 
    35 ## main
    36 
    37 if [ -z "$DOC" ]; then
    38   for DIR in $ISABELLE_DOCS
    39   do
    40     [ -f $DIR/Contents ] && cat $DIR/Contents
    41   done
    42 else
    43   for DIR in $ISABELLE_DOCS
    44   do
    45     [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    46   done
    47   fail "Unknown Isabelle document: $DOC"  
    48 fi