lib/Tools/display
author paulson
Fri Oct 01 11:54:15 2004 +0200 (2004-10-01)
changeset 15223 e669fb5b0f5a
parent 15218 39747a9e3c37
child 15703 727ef1b8b3ee
permissions -rwxr-xr-x
patch to "display"
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
kleing@15218
    31
function view()
kleing@15218
    32
{
kleing@15218
    33
  if [ "${1%%.dvi}.dvi" == "$1" ]; then
kleing@15218
    34
    exec $DVI_VIEWER "$1"
kleing@15218
    35
    return
kleing@15218
    36
  fi
kleing@15218
    37
kleing@15218
    38
  if [ "${1%%.pdf}.pdf" == "$1" ]; then
kleing@15218
    39
    exec $PDF_VIEWER "$1"
kleing@15218
    40
    return
kleing@15218
    41
  fi
kleing@15218
    42
kleing@15218
    43
  fail "Unknown file type: $FILE";
kleing@15218
    44
}
kleing@15218
    45
wenzelm@14930
    46
## process command line
wenzelm@14930
    47
wenzelm@14930
    48
# options
wenzelm@14930
    49
wenzelm@14930
    50
CLEAN=""
wenzelm@14930
    51
wenzelm@14930
    52
while getopts "c" OPT
wenzelm@14930
    53
do
wenzelm@14930
    54
  case "$OPT" in
wenzelm@14930
    55
    c)
wenzelm@14930
    56
      CLEAN=true
wenzelm@14930
    57
      ;;
wenzelm@14930
    58
    \?)
wenzelm@14930
    59
      usage
wenzelm@14930
    60
      ;;
wenzelm@14930
    61
  esac
wenzelm@14930
    62
done
wenzelm@14930
    63
wenzelm@14930
    64
shift $(($OPTIND - 1))
wenzelm@14930
    65
wenzelm@14930
    66
wenzelm@14930
    67
# args
wenzelm@14930
    68
wenzelm@14930
    69
[ "$#" -ne 1 ] && usage
wenzelm@14930
    70
wenzelm@14930
    71
FILE="$1"; shift
wenzelm@14930
    72
wenzelm@14930
    73
wenzelm@14930
    74
## main
wenzelm@14930
    75
wenzelm@14930
    76
[ -f "$FILE" ] || fail "Bad file: $FILE"
wenzelm@14930
    77
wenzelm@14930
    78
if [ -n "$CLEAN" ]; then
paulson@15223
    79
  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE")
paulson@15223
    80
  mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE"
kleing@15218
    81
  view "$PRIVATE_FILE"
wenzelm@14930
    82
  rm -f "$PRIVATE_FILE"
wenzelm@14930
    83
else
kleing@15218
    84
  view "$FILE"
wenzelm@14930
    85
fi