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