lib/Tools/display
author blanchet
Wed May 21 14:09:42 2014 +0200 (2014-05-21)
changeset 57037 c51132be8e16
parent 54683 cf48ddc266e5
permissions -rwxr-xr-x
avoid markup-generating @{make_string}
wenzelm@14930
     1
#!/usr/bin/env bash
wenzelm@14930
     2
#
wenzelm@54683
     3
# Author: Makarius
wenzelm@14930
     4
#
kleing@15218
     5
# DESCRIPTION: display document (in DVI or PDF format)
wenzelm@14930
     6
wenzelm@14930
     7
wenzelm@14930
     8
PRG="$(basename "$0")"
wenzelm@14930
     9
wenzelm@14930
    10
function usage()
wenzelm@14930
    11
{
wenzelm@14930
    12
  echo
wenzelm@54683
    13
  echo "Usage: isabelle $PRG DOCUMENT"
wenzelm@14930
    14
  echo
wenzelm@54683
    15
  echo "  Display DOCUMENT (in DVI or PDF format)."
wenzelm@14930
    16
  echo
wenzelm@14930
    17
  exit 1
wenzelm@14930
    18
}
wenzelm@14930
    19
wenzelm@14930
    20
function fail()
wenzelm@14930
    21
{
wenzelm@14930
    22
  echo "$1" >&2
wenzelm@14930
    23
  exit 2
wenzelm@14930
    24
}
wenzelm@14930
    25
wenzelm@14930
    26
wenzelm@14930
    27
## main
wenzelm@14930
    28
wenzelm@54683
    29
[ "$#" -ne 1 -o "$1" = "-?" ] && usage
wenzelm@54683
    30
wenzelm@54683
    31
DOCUMENT="$1"; shift
wenzelm@54683
    32
wenzelm@54683
    33
[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
wenzelm@14930
    34
wenzelm@54683
    35
case "$DOCUMENT" in
wenzelm@54683
    36
  *.dvi)
wenzelm@54683
    37
    exec "$DVI_VIEWER" "$DOCUMENT"
wenzelm@54683
    38
    ;;
wenzelm@54683
    39
  *.pdf)
wenzelm@54683
    40
    exec "$PDF_VIEWER" "$DOCUMENT"
wenzelm@54683
    41
    ;;
wenzelm@54683
    42
  *)
wenzelm@54683
    43
    fail "Unknown document type: \"$DOCUMENT\"";
wenzelm@15703
    44
esac
wenzelm@15703
    45