#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: display document (in DVI or PDF format)
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG DOCUMENT"
echo
echo " Display DOCUMENT (in DVI or PDF format)."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## main
[ "$#" -ne 1 -o "$1" = "-?" ] && usage
DOCUMENT="$1"; shift
[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
case "$DOCUMENT" in
*.dvi)
exec "$DVI_VIEWER" "$DOCUMENT"
;;
*.pdf)
exec "$PDF_VIEWER" "$DOCUMENT"
;;
*)
fail "Unknown document type: \"$DOCUMENT\"";
esac