author | wenzelm |
Mon, 15 Oct 2001 20:35:10 +0200 | |
changeset 11781 | a08b62908caa |
parent 11581 | d7bb261e3a3b |
child 11844 | eb072fd9a45a |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
7793 | 2 |
# |
3 |
# $Id$ |
|
9788 | 4 |
# Author: Markus Wenzel, TU Muenchen |
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
7793 | 6 |
# |
7 |
# DESCRIPTION: prepare theory session document |
|
8 |
||
9 |
||
10511 | 10 |
PRG="$(basename "$0")" |
7793 | 11 |
|
12 |
function usage() |
|
13 |
{ |
|
14 |
echo |
|
15 |
echo "Usage: $PRG [OPTIONS] [DIR]" |
|
16 |
echo |
|
17 |
echo " Options are:" |
|
8654 | 18 |
echo " -c cleanup -- be aggressive in removing old stuff" |
7866
3ccaa11b6df9
pdf: generate thumbnails if ISABELLE_THUMBPDF set;
wenzelm
parents:
7857
diff
changeset
|
19 |
echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
3ccaa11b6df9
pdf: generate thumbnails if ISABELLE_THUMBPDF set;
wenzelm
parents:
7857
diff
changeset
|
20 |
echo " ps.gz, pdf" |
11581 | 21 |
echo " -v be verbose" |
7793 | 22 |
echo |
8211 | 23 |
echo " Prepare the theory session document in DIR (default 'document')" |
7857 | 24 |
echo " producing the specified output format." |
7793 | 25 |
echo |
26 |
exit 1 |
|
27 |
} |
|
28 |
||
29 |
function fail() |
|
30 |
{ |
|
31 |
echo "$1" >&2 |
|
32 |
exit 2 |
|
33 |
} |
|
34 |
||
35 |
||
36 |
## process command line |
|
37 |
||
38 |
# options |
|
39 |
||
8211 | 40 |
CLEAN="" |
7793 | 41 |
OUTFORMAT=dvi |
11581 | 42 |
VERBOSE="" |
7793 | 43 |
|
11581 | 44 |
while getopts "co:v" OPT |
7793 | 45 |
do |
46 |
case "$OPT" in |
|
8211 | 47 |
c) |
48 |
CLEAN=true |
|
49 |
;; |
|
7793 | 50 |
o) |
51 |
OUTFORMAT="$OPTARG" |
|
52 |
;; |
|
11581 | 53 |
v) |
54 |
VERBOSE=true |
|
55 |
;; |
|
7793 | 56 |
\?) |
57 |
usage |
|
58 |
;; |
|
59 |
esac |
|
60 |
done |
|
61 |
||
62 |
shift $(($OPTIND - 1)) |
|
63 |
||
64 |
||
65 |
# args |
|
66 |
||
8211 | 67 |
DIR="document" |
9788 | 68 |
[ "$#" -ge 1 ] && { DIR="$1"; shift; } |
7793 | 69 |
|
9788 | 70 |
[ "$#" -ne 0 ] && usage |
7793 | 71 |
|
72 |
||
73 |
## main |
|
74 |
||
7814 | 75 |
# check format |
76 |
||
77 |
case "$OUTFORMAT" in |
|
78 |
dvi | dvi.gz | ps | ps.gz | pdf) |
|
79 |
;; |
|
80 |
*) |
|
81 |
fail "Bad output format '$OUTFORMAT'" |
|
82 |
;; |
|
83 |
esac |
|
84 |
||
85 |
||
86 |
# prepare document |
|
7793 | 87 |
|
7814 | 88 |
function pre_latex () |
89 |
{ |
|
90 |
local FMT="$1" |
|
8654 | 91 |
[ -n "$CLEAN" ] && rm -f *.aux *.out |
7814 | 92 |
if [ -f root.bib ] |
93 |
then |
|
9788 | 94 |
"$ISATOOL" latex -o "$FMT" && \ |
95 |
"$ISATOOL" latex -o bbl && \ |
|
96 |
"$ISATOOL" latex -o "$FMT" |
|
7814 | 97 |
else |
9788 | 98 |
"$ISATOOL" latex -o "$FMT" |
7814 | 99 |
fi |
100 |
} |
|
101 |
||
8211 | 102 |
( |
103 |
cd "$DIR" || fail "Bad directory '$DIR'" |
|
104 |
||
8654 | 105 |
[ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT" |
106 |
||
8211 | 107 |
if [ -f IsaMakefile ]; then |
9788 | 108 |
"$ISATOOL" make "$OUTFORMAT" |
109 |
RC="$?" |
|
8211 | 110 |
elif [ "$OUTFORMAT" = pdf ]; then |
111 |
pre_latex pdf && \ |
|
9788 | 112 |
"$ISATOOL" latex -o pdf && \ |
8211 | 113 |
{ if [ -n "$ISABELLE_THUMBPDF" ]; then |
9788 | 114 |
"$ISATOOL" latex -o png && \ |
115 |
"$ISATOOL" latex -o pdf |
|
8211 | 116 |
fi; } |
9788 | 117 |
RC="$?" |
8211 | 118 |
else |
119 |
pre_latex dvi && \ |
|
9788 | 120 |
"$ISATOOL" latex -o "$OUTFORMAT" |
121 |
RC="$?" |
|
8211 | 122 |
fi |
123 |
||
11581 | 124 |
if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then |
125 |
cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \ |
|
126 |
[ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2 |
|
127 |
fi |
|
8211 | 128 |
|
8217 | 129 |
exit "$RC" |
8211 | 130 |
) |
9788 | 131 |
RC="$?" |
7793 | 132 |
|
133 |
||
7814 | 134 |
# install |
7793 | 135 |
|
8211 | 136 |
[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'" |
137 |
||
138 |
#beware! |
|
139 |
[ -n "$CLEAN" ] && rm -rf "$DIR" |
|
140 |
||
141 |
exit "$RC" |