lib/Tools/doc
author wenzelm
Mon May 12 18:43:24 1997 +0200 (1997-05-12)
changeset 3173 0013af1bc2c4
parent 3007 e5efa177ee0c
child 8130 b077b79061b6
permissions -rwxr-xr-x
fixed ISABELLE_DOCS multiple components;
     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 DOCS=$(echo $ISABELLE_DOCS | tr : " ")
    38 
    39 if [ -z "$DOC" ]; then
    40   for DIR in $DOCS
    41   do
    42     [ -f $DIR/Contents ] && cat $DIR/Contents
    43   done
    44 else
    45   for DIR in $DOCS
    46   do
    47     [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    48   done
    49   fail "Unknown Isabelle document: $DOC"  
    50 fi