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