author | wenzelm |
Tue, 25 Oct 2016 17:22:05 +0200 | |
changeset 64398 | 5076725247fa |
parent 54683 | cf48ddc266e5 |
permissions | -rwxr-xr-x |
14930 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
3 |
# Author: Makarius |
14930 | 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 |
|
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
13 |
echo "Usage: isabelle $PRG DOCUMENT" |
14930 | 14 |
echo |
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
15 |
echo " Display DOCUMENT (in DVI or PDF format)." |
14930 | 16 |
echo |
17 |
exit 1 |
|
18 |
} |
|
19 |
||
20 |
function fail() |
|
21 |
{ |
|
22 |
echo "$1" >&2 |
|
23 |
exit 2 |
|
24 |
} |
|
25 |
||
26 |
||
27 |
## main |
|
28 |
||
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
29 |
[ "$#" -ne 1 -o "$1" = "-?" ] && usage |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
30 |
|
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
31 |
DOCUMENT="$1"; shift |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
32 |
|
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
33 |
[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\"" |
14930 | 34 |
|
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
35 |
case "$DOCUMENT" in |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
36 |
*.dvi) |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
37 |
exec "$DVI_VIEWER" "$DOCUMENT" |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
38 |
;; |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
39 |
*.pdf) |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
40 |
exec "$PDF_VIEWER" "$DOCUMENT" |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
41 |
;; |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
42 |
*) |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
50197
diff
changeset
|
43 |
fail "Unknown document type: \"$DOCUMENT\""; |
15703 | 44 |
esac |
45 |