lib/Tools/doc
author wenzelm
Thu Nov 30 20:10:29 2000 +0100 (2000-11-30)
changeset 10555 2323ec838401
parent 10511 efb3428c9879
child 14981 e73f8140af78
permissions -rwxr-xr-x
/usr/bin/env bash;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: view Isabelle documentation
     8 
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [DOC]"
    16   echo
    17   echo "  View Isabelle documentation DOC, or show list of available documents."
    18   echo
    19   exit 1
    20 }
    21 
    22 function fail()
    23 {
    24   echo "$1" >&2
    25   exit 2
    26 }
    27 
    28 
    29 ## args
    30 
    31 DOC=""
    32 [ "$#" -ge 1 ] && { DOC="$1"; shift; }
    33 
    34 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
    35 
    36 
    37 ## main
    38 
    39 if [ -z "$DOC" ]; then
    40   ORIG_IFS="$IFS"
    41   IFS=":"
    42   for DIR in $ISABELLE_DOCS
    43   do
    44     [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
    45   done
    46   IFS="$ORIG_IFS"
    47 else
    48   ORIG_IFS="$IFS"
    49   IFS=":"
    50   for DIR in $ISABELLE_DOCS
    51   do
    52     [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
    53   done
    54   IFS="$ORIG_IFS"
    55   fail "Unknown Isabelle document: $DOC"  
    56 fi