lib/Tools/doc
author wenzelm
Mon Dec 09 09:02:15 1996 +0100 (1996-12-09)
changeset 2332 ae592411c199
child 2916 d761a62da697
permissions -rwxr-xr-x
doc: view Isabelle documentation;
wenzelm@2332
     1
#!/bin/bash -norc
wenzelm@2332
     2
#
wenzelm@2332
     3
# $Id$
wenzelm@2332
     4
#
wenzelm@2332
     5
# DESCRIPTION: view Isabelle documentation
wenzelm@2332
     6
#
wenzelm@2332
     7
# TODO:
wenzelm@2332
     8
#  - other formats than dvi (??)
wenzelm@2332
     9
wenzelm@2332
    10
wenzelm@2332
    11
PRG=$(basename $0)
wenzelm@2332
    12
wenzelm@2332
    13
function usage()
wenzelm@2332
    14
{
wenzelm@2332
    15
  echo
wenzelm@2332
    16
  echo "Usage: $PRG [DOC]"
wenzelm@2332
    17
  echo
wenzelm@2332
    18
  echo "  View Isabelle documentation DOC, or show list of available documents."
wenzelm@2332
    19
  echo
wenzelm@2332
    20
  exit 1
wenzelm@2332
    21
}
wenzelm@2332
    22
wenzelm@2332
    23
function fail()
wenzelm@2332
    24
{
wenzelm@2332
    25
  echo "$1" >&2
wenzelm@2332
    26
  exit 2
wenzelm@2332
    27
}
wenzelm@2332
    28
wenzelm@2332
    29
wenzelm@2332
    30
## args
wenzelm@2332
    31
wenzelm@2332
    32
DOC=""
wenzelm@2332
    33
[ $# -ge 1 ] && { DOC="$1"; shift }
wenzelm@2332
    34
wenzelm@2332
    35
[ $# -ne 0 -o "$DOC" = "-?" ] && usage
wenzelm@2332
    36
wenzelm@2332
    37
wenzelm@2332
    38
## main
wenzelm@2332
    39
wenzelm@2332
    40
if [ -z "$DOC" ]; then
wenzelm@2332
    41
  for DIR in $ISABELLE_DOCS
wenzelm@2332
    42
  do
wenzelm@2332
    43
    [ -f $DIR/Contents ] && cat $DIR/Contents
wenzelm@2332
    44
  done
wenzelm@2332
    45
else
wenzelm@2332
    46
  for DIR in $ISABELLE_DOCS
wenzelm@2332
    47
  do
wenzelm@2332
    48
    [ -f $DIR/$DOC.dvi ] && exec $DVI_VIEWER $DIR/$DOC.dvi
wenzelm@2332
    49
  done
wenzelm@2332
    50
  fail "Unknown Isabelle document: $DOC"  
wenzelm@2332
    51
fi