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