author | wenzelm |
Fri, 21 May 2010 23:21:40 +0200 | |
changeset 37056 | d03b57457421 |
parent 29143 | 72c960b2b83e |
child 44987 | fd3a36e48b09 |
permissions | -rwxr-xr-x |
14930 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Markus Wenzel, TU Muenchen |
|
4 |
# |
|
15218 | 5 |
# DESCRIPTION: display document (in DVI or PDF format) |
14930 | 6 |
|
7 |
||
8 |
PRG="$(basename "$0")" |
|
9 |
||
10 |
function usage() |
|
11 |
{ |
|
12 |
echo |
|
28650 | 13 |
echo "Usage: isabelle $PRG [OPTIONS] FILE" |
14930 | 14 |
echo |
15 |
echo " Options are:" |
|
16 |
echo " -c cleanup -- remove FILE after use" |
|
17 |
echo |
|
15218 | 18 |
echo " Display document FILE (in DVI or PDF format)." |
14930 | 19 |
echo |
20 |
exit 1 |
|
21 |
} |
|
22 |
||
23 |
function fail() |
|
24 |
{ |
|
25 |
echo "$1" >&2 |
|
26 |
exit 2 |
|
27 |
} |
|
28 |
||
29 |
||
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 |
|
59 |
||
60 |
[ -f "$FILE" ] || fail "Bad file: $FILE" |
|
61 |
||
15703 | 62 |
case "$FILE" in |
63 |
*.dvi) |
|
64 |
VIEWER="$DVI_VIEWER" |
|
65 |
;; |
|
66 |
*.pdf) |
|
67 |
VIEWER="$PDF_VIEWER" |
|
68 |
;; |
|
69 |
*) |
|
70 |
fail "Unknown file type: $FILE"; |
|
71 |
esac |
|
72 |
||
14930 | 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 | 75 |
mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
76 |
$VIEWER "$PRIVATE_FILE" |
|
21342 | 77 |
sleep 5 #try to avoid races |
14930 | 78 |
rm -f "$PRIVATE_FILE" |
79 |
else |
|
15703 | 80 |
exec $VIEWER "$FILE" |
14930 | 81 |
fi |