lib/Tools/display
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 50197 b385d134926d
child 54683 cf48ddc266e5
permissions -rwxr-xr-x
tuned;
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
# Author: Markus Wenzel, TU Muenchen
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     4
#
15218
39747a9e3c37 display pdf as well as dvi
kleing
parents: 15010
diff changeset
     5
# DESCRIPTION: display document (in DVI or PDF format)
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     6
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     7
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     8
PRG="$(basename "$0")"
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     9
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    10
function usage()
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    11
{
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 21342
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] FILE"
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    14
  echo
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    15
  echo "  Options are:"
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    16
  echo "    -c           cleanup -- remove FILE after use"
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    17
  echo
15218
39747a9e3c37 display pdf as well as dvi
kleing
parents: 15010
diff changeset
    18
  echo "  Display document FILE (in DVI or PDF format)."
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    19
  echo
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    20
  exit 1
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    21
}
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    22
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    23
function fail()
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    24
{
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    25
  echo "$1" >&2
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    26
  exit 2
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    27
}
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
## process command line
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    31
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    32
# options
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    33
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    34
CLEAN=""
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    35
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    36
while getopts "c" OPT
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    37
do
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    38
  case "$OPT" in
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    39
    c)
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    40
      CLEAN=true
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    41
      ;;
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    42
    \?)
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    43
      usage
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    44
      ;;
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    45
  esac
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    46
done
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    47
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    48
shift $(($OPTIND - 1))
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    49
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    50
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    51
# args
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    52
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    53
[ "$#" -ne 1 ] && usage
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    54
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    55
FILE="$1"; shift
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    56
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    57
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    58
## main
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    59
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    60
[ -f "$FILE" ] || fail "Bad file: $FILE"
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    61
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    62
case "$FILE" in
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    63
    *.dvi)
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    64
      VIEWER="$DVI_VIEWER"
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    65
      ;;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    66
    *.pdf)
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    67
      VIEWER="$PDF_VIEWER"
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    68
      ;;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    69
    *)
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    70
      fail "Unknown file type: $FILE";
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    71
esac
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    72
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    73
if [ -n "$CLEAN" ]; then
20570
f78dfa306918 PRIVATE_FILE: slightly more robust way to create and dispose;
wenzelm
parents: 15718
diff changeset
    74
  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    75
  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
50197
b385d134926d eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
wenzelm
parents: 47884
diff changeset
    76
  eval "$VIEWER \"$PRIVATE_FILE\""
47884
21c42b095c84 try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
wenzelm
parents: 44987
diff changeset
    77
  sleep 5   #try to avoid races
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
50197
b385d134926d eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
wenzelm
parents: 47884
diff changeset
    80
  eval "$VIEWER \"$FILE\""
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    81
fi