lib/Tools/display
author wenzelm
Sun Jun 13 15:28:12 2004 +0200 (2004-06-13)
changeset 14930 24a0b2dd9be6
child 14951 c98eb0d6615a
permissions -rwxr-xr-x
display document (in DVI format)
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
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@14930
     6
#
wenzelm@14930
     7
# DESCRIPTION: display document (in DVI format)
wenzelm@14930
     8
wenzelm@14930
     9
wenzelm@14930
    10
PRG="$(basename "$0")"
wenzelm@14930
    11
wenzelm@14930
    12
function usage()
wenzelm@14930
    13
{
wenzelm@14930
    14
  echo
wenzelm@14930
    15
  echo "Usage: $PRG [OPTIONS] FILE"
wenzelm@14930
    16
  echo
wenzelm@14930
    17
  echo "  Options are:"
wenzelm@14930
    18
  echo "    -c           cleanup -- remove FILE after use"
wenzelm@14930
    19
  echo
wenzelm@14930
    20
  echo "  Display document FILE (in DVI format)."
wenzelm@14930
    21
  echo
wenzelm@14930
    22
  exit 1
wenzelm@14930
    23
}
wenzelm@14930
    24
wenzelm@14930
    25
function fail()
wenzelm@14930
    26
{
wenzelm@14930
    27
  echo "$1" >&2
wenzelm@14930
    28
  exit 2
wenzelm@14930
    29
}
wenzelm@14930
    30
wenzelm@14930
    31
wenzelm@14930
    32
## process command line
wenzelm@14930
    33
wenzelm@14930
    34
# options
wenzelm@14930
    35
wenzelm@14930
    36
CLEAN=""
wenzelm@14930
    37
wenzelm@14930
    38
while getopts "c" OPT
wenzelm@14930
    39
do
wenzelm@14930
    40
  case "$OPT" in
wenzelm@14930
    41
    c)
wenzelm@14930
    42
      CLEAN=true
wenzelm@14930
    43
      ;;
wenzelm@14930
    44
    \?)
wenzelm@14930
    45
      usage
wenzelm@14930
    46
      ;;
wenzelm@14930
    47
  esac
wenzelm@14930
    48
done
wenzelm@14930
    49
wenzelm@14930
    50
shift $(($OPTIND - 1))
wenzelm@14930
    51
wenzelm@14930
    52
wenzelm@14930
    53
# args
wenzelm@14930
    54
wenzelm@14930
    55
[ "$#" -ne 1 ] && usage
wenzelm@14930
    56
wenzelm@14930
    57
FILE="$1"; shift
wenzelm@14930
    58
wenzelm@14930
    59
wenzelm@14930
    60
## main
wenzelm@14930
    61
wenzelm@14930
    62
[ -f "$FILE" ] || fail "Bad file: $FILE"
wenzelm@14930
    63
wenzelm@14930
    64
if [ -n "$CLEAN" ]; then
wenzelm@14930
    65
  PRIVATE_FILE=$(basename "$FILE" .dvi)$$.dvi
wenzelm@14930
    66
  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
wenzelm@14930
    67
  $DVI_VIEWER "$PRIVATE_FILE"
wenzelm@14930
    68
  rm -f "$PRIVATE_FILE"
wenzelm@14930
    69
else
wenzelm@14930
    70
  exec $DVI_VIEWER "$FILE"
wenzelm@14930
    71
fi