lib/Tools/doc
author wenzelm
Mon Jan 17 15:02:18 2000 +0100 (2000-01-17)
changeset 8130 b077b79061b6
parent 3173 0013af1bc2c4
child 9788 df671fa2562a
permissions -rwxr-xr-x
Contents: suppress comments;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2332
     2
#
wenzelm@2332
     3
# $Id$
wenzelm@2332
     4
#
wenzelm@2332
     5
# DESCRIPTION: view Isabelle documentation
wenzelm@2332
     6
wenzelm@2332
     7
wenzelm@2332
     8
PRG=$(basename $0)
wenzelm@2332
     9
wenzelm@2332
    10
function usage()
wenzelm@2332
    11
{
wenzelm@2332
    12
  echo
wenzelm@2332
    13
  echo "Usage: $PRG [DOC]"
wenzelm@2332
    14
  echo
wenzelm@2332
    15
  echo "  View Isabelle documentation DOC, or show list of available documents."
wenzelm@2332
    16
  echo
wenzelm@2332
    17
  exit 1
wenzelm@2332
    18
}
wenzelm@2332
    19
wenzelm@2332
    20
function fail()
wenzelm@2332
    21
{
wenzelm@2332
    22
  echo "$1" >&2
wenzelm@2332
    23
  exit 2
wenzelm@2332
    24
}
wenzelm@2332
    25
wenzelm@2332
    26
wenzelm@2332
    27
## args
wenzelm@2332
    28
wenzelm@2332
    29
DOC=""
wenzelm@2936
    30
[ $# -ge 1 ] && { DOC="$1"; shift; }
wenzelm@2332
    31
wenzelm@2332
    32
[ $# -ne 0 -o "$DOC" = "-?" ] && usage
wenzelm@2332
    33
wenzelm@2332
    34
wenzelm@2332
    35
## main
wenzelm@2332
    36
wenzelm@3173
    37
DOCS=$(echo $ISABELLE_DOCS | tr : " ")
wenzelm@3173
    38
wenzelm@2332
    39
if [ -z "$DOC" ]; then
wenzelm@3173
    40
  for DIR in $DOCS
wenzelm@2332
    41
  do
wenzelm@8130
    42
    [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
wenzelm@2332
    43
  done
wenzelm@2332
    44
else
wenzelm@3173
    45
  for DIR in $DOCS
wenzelm@2332
    46
  do
wenzelm@2936
    47
    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
wenzelm@2332
    48
  done
wenzelm@2332
    49
  fail "Unknown Isabelle document: $DOC"  
wenzelm@2332
    50
fi