1#!/usr/bin/env bash
2#
3# Author: Makarius
4#
5# DESCRIPTION: display document (in DVI or PDF format)
6
7
8PRG="$(basename "$0")"
9
10function usage()
11{
12  echo
13  echo "Usage: isabelle $PRG DOCUMENT"
14  echo
15  echo "  Display DOCUMENT (in DVI or PDF format)."
16  echo
17  exit 1
18}
19
20function fail()
21{
22  echo "$1" >&2
23  exit 2
24}
25
26
27## main
28
29[ "$#" -ne 1 -o "$1" = "-?" ] && usage
30
31DOCUMENT="$1"; shift
32
33[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
34
35case "$DOCUMENT" in
36  *.dvi)
37    exec "$DVI_VIEWER" "$DOCUMENT"
38    ;;
39  *.pdf)
40    exec "$PDF_VIEWER" "$DOCUMENT"
41    ;;
42  *)
43    fail "Unknown document type: \"$DOCUMENT\"";
44esac
45
46