equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Markus Wenzel, TU Muenchen |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: display document (in DVI or PDF format) |
5 # DESCRIPTION: display document (in DVI or PDF format) |
6 |
6 |
7 |
7 |
8 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: isabelle $PRG [OPTIONS] FILE" |
13 echo "Usage: isabelle $PRG DOCUMENT" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Display DOCUMENT (in DVI or PDF format)." |
16 echo " -c cleanup -- remove FILE after use" |
|
17 echo |
|
18 echo " Display document FILE (in DVI or PDF format)." |
|
19 echo |
16 echo |
20 exit 1 |
17 exit 1 |
21 } |
18 } |
22 |
19 |
23 function fail() |
20 function fail() |
25 echo "$1" >&2 |
22 echo "$1" >&2 |
26 exit 2 |
23 exit 2 |
27 } |
24 } |
28 |
25 |
29 |
26 |
30 ## process command line |
|
31 |
|
32 # options |
|
33 |
|
34 CLEAN="" |
|
35 |
|
36 while getopts "c" OPT |
|
37 do |
|
38 case "$OPT" in |
|
39 c) |
|
40 CLEAN=true |
|
41 ;; |
|
42 \?) |
|
43 usage |
|
44 ;; |
|
45 esac |
|
46 done |
|
47 |
|
48 shift $(($OPTIND - 1)) |
|
49 |
|
50 |
|
51 # args |
|
52 |
|
53 [ "$#" -ne 1 ] && usage |
|
54 |
|
55 FILE="$1"; shift |
|
56 |
|
57 |
|
58 ## main |
27 ## main |
59 |
28 |
60 [ -f "$FILE" ] || fail "Bad file: $FILE" |
29 [ "$#" -ne 1 -o "$1" = "-?" ] && usage |
61 |
30 |
62 case "$FILE" in |
31 DOCUMENT="$1"; shift |
63 *.dvi) |
32 |
64 VIEWER="$DVI_VIEWER" |
33 [ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\"" |
65 ;; |
34 |
66 *.pdf) |
35 case "$DOCUMENT" in |
67 VIEWER="$PDF_VIEWER" |
36 *.dvi) |
68 ;; |
37 exec "$DVI_VIEWER" "$DOCUMENT" |
69 *) |
38 ;; |
70 fail "Unknown file type: $FILE"; |
39 *.pdf) |
|
40 exec "$PDF_VIEWER" "$DOCUMENT" |
|
41 ;; |
|
42 *) |
|
43 fail "Unknown document type: \"$DOCUMENT\""; |
71 esac |
44 esac |
72 |
45 |
73 if [ -n "$CLEAN" ]; then |
|
74 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE") |
|
75 mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
|
76 eval "$VIEWER \"$PRIVATE_FILE\"" |
|
77 sleep 5 #try to avoid races |
|
78 rm -f "$PRIVATE_FILE" |
|
79 else |
|
80 eval "$VIEWER \"$FILE\"" |
|
81 fi |
|