lib/Tools/display
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15223 e669fb5b0f5a
child 15718 f088c10208c0
permissions -rwxr-xr-x
*** empty log message ***
wenzelm@14930
     1
#!/usr/bin/env bash
wenzelm@14930
     2
#
wenzelm@14930
     3
# $Id$
wenzelm@14930
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@14930
     5
#
kleing@15218
     6
# DESCRIPTION: display document (in DVI or PDF format)
wenzelm@14930
     7
wenzelm@14930
     8
wenzelm@14930
     9
PRG="$(basename "$0")"
wenzelm@14930
    10
wenzelm@14930
    11
function usage()
wenzelm@14930
    12
{
wenzelm@14930
    13
  echo
wenzelm@14930
    14
  echo "Usage: $PRG [OPTIONS] FILE"
wenzelm@14930
    15
  echo
wenzelm@14930
    16
  echo "  Options are:"
wenzelm@14930
    17
  echo "    -c           cleanup -- remove FILE after use"
wenzelm@14930
    18
  echo
kleing@15218
    19
  echo "  Display document FILE (in DVI or PDF format)."
wenzelm@14930
    20
  echo
wenzelm@14930
    21
  exit 1
wenzelm@14930
    22
}
wenzelm@14930
    23
wenzelm@14930
    24
function fail()
wenzelm@14930
    25
{
wenzelm@14930
    26
  echo "$1" >&2
wenzelm@14930
    27
  exit 2
wenzelm@14930
    28
}
wenzelm@14930
    29
wenzelm@14930
    30
wenzelm@14930
    31
## process command line
wenzelm@14930
    32
wenzelm@14930
    33
# options
wenzelm@14930
    34
wenzelm@14930
    35
CLEAN=""
wenzelm@14930
    36
wenzelm@14930
    37
while getopts "c" OPT
wenzelm@14930
    38
do
wenzelm@14930
    39
  case "$OPT" in
wenzelm@14930
    40
    c)
wenzelm@14930
    41
      CLEAN=true
wenzelm@14930
    42
      ;;
wenzelm@14930
    43
    \?)
wenzelm@14930
    44
      usage
wenzelm@14930
    45
      ;;
wenzelm@14930
    46
  esac
wenzelm@14930
    47
done
wenzelm@14930
    48
wenzelm@14930
    49
shift $(($OPTIND - 1))
wenzelm@14930
    50
wenzelm@14930
    51
wenzelm@14930
    52
# args
wenzelm@14930
    53
wenzelm@14930
    54
[ "$#" -ne 1 ] && usage
wenzelm@14930
    55
wenzelm@14930
    56
FILE="$1"; shift
wenzelm@14930
    57
wenzelm@14930
    58
wenzelm@14930
    59
## main
wenzelm@14930
    60
wenzelm@14930
    61
[ -f "$FILE" ] || fail "Bad file: $FILE"
wenzelm@14930
    62
wenzelm@15703
    63
case "$FILE" in
wenzelm@15703
    64
    *.dvi)
wenzelm@15703
    65
      VIEWER="$DVI_VIEWER"
wenzelm@15703
    66
      ;;
wenzelm@15703
    67
    *.pdf)
wenzelm@15703
    68
      VIEWER="$PDF_VIEWER"
wenzelm@15703
    69
      ;;
wenzelm@15703
    70
    *)
wenzelm@15703
    71
      fail "Unknown file type: $FILE";
wenzelm@15703
    72
esac
wenzelm@15703
    73
wenzelm@14930
    74
if [ -n "$CLEAN" ]; then
wenzelm@15703
    75
  PRIVATE_FILE="$ISABELLE_TMP/$$"$(basename "$FILE")
wenzelm@15703
    76
  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
wenzelm@15703
    77
  $VIEWER "$PRIVATE_FILE"
wenzelm@14930
    78
  rm -f "$PRIVATE_FILE"
wenzelm@14930
    79
else
wenzelm@15703
    80
  exec $VIEWER "$FILE"
wenzelm@14930
    81
fi