lib/Tools/doc
changeset 9788 df671fa2562a
parent 8130 b077b79061b6
child 10511 efb3428c9879
equal deleted inserted replaced
9787:fb8c5a66dbe8 9788:df671fa2562a
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # DESCRIPTION: view Isabelle documentation
     7 # DESCRIPTION: view Isabelle documentation
     6 
     8 
     7 
     9 
     8 PRG=$(basename $0)
    10 PRG=$(basename "$0")
     9 
    11 
    10 function usage()
    12 function usage()
    11 {
    13 {
    12   echo
    14   echo
    13   echo "Usage: $PRG [DOC]"
    15   echo "Usage: $PRG [DOC]"
    25 
    27 
    26 
    28 
    27 ## args
    29 ## args
    28 
    30 
    29 DOC=""
    31 DOC=""
    30 [ $# -ge 1 ] && { DOC="$1"; shift; }
    32 [ "$#" -ge 1 ] && { DOC="$1"; shift; }
    31 
    33 
    32 [ $# -ne 0 -o "$DOC" = "-?" ] && usage
    34 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
    33 
    35 
    34 
    36 
    35 ## main
    37 ## main
    36 
    38 
    37 DOCS=$(echo $ISABELLE_DOCS | tr : " ")
       
    38 
       
    39 if [ -z "$DOC" ]; then
    39 if [ -z "$DOC" ]; then
    40   for DIR in $DOCS
    40   ORIG_IFS="$IFS"
       
    41   IFS=":"
       
    42   for DIR in $ISABELLE_DOCS
    41   do
    43   do
    42     [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
    44     [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
    43   done
    45   done
       
    46   IFS="$ORIG_IFS"
    44 else
    47 else
    45   for DIR in $DOCS
    48   ORIG_IFS="$IFS"
       
    49   IFS=":"
       
    50   for DIR in $ISABELLE_DOCS
    46   do
    51   do
    47     [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    52     [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
    48   done
    53   done
       
    54   IFS="$ORIG_IFS"
    49   fail "Unknown Isabelle document: $DOC"  
    55   fail "Unknown Isabelle document: $DOC"  
    50 fi
    56 fi