#!/bin/bash
#
# $Id$
#
# DESCRIPTION: view Isabelle documentation
PRG=$(basename $0)
function usage()
{
echo
echo "Usage: $PRG [DOC]"
echo
echo " View Isabelle documentation DOC, or show list of available documents."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## args
DOC=""
[ $# -ge 1 ] && { DOC="$1"; shift; }
[ $# -ne 0 -o "$DOC" = "-?" ] && usage
## main
DOCS=$(echo $ISABELLE_DOCS | tr : " ")
if [ -z "$DOC" ]; then
for DIR in $DOCS
do
[ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
done
else
for DIR in $DOCS
do
[ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
done
fail "Unknown Isabelle document: $DOC"
fi