lib/Tools/doc
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 14981 e73f8140af78
child 15717 541e50adfc73
permissions -rwxr-xr-x
*** empty log message ***
     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     [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    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     IFS="$ORIG_IFS"
    53     [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    54     for FMT in "$ISABELLE_DOC_FORMAT" dvi
    55     do
    56       [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; }
    57     done
    58   done
    59   IFS="$ORIG_IFS"
    60   fail "Unknown Isabelle document: $DOC"  
    61 fi