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