lib/Tools/display
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 54683 cf48ddc266e5
permissions -rwxr-xr-x
updated for release;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: display document (in DVI or PDF format)
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function 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 
    20 function fail()
    21 {
    22   echo "$1" >&2
    23   exit 2
    24 }
    25 
    26 
    27 ## main
    28 
    29 [ "$#" -ne 1 -o "$1" = "-?" ] && usage
    30 
    31 DOCUMENT="$1"; shift
    32 
    33 [ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
    34 
    35 case "$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\"";
    44 esac
    45