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