author | wenzelm |
Sun, 20 Jun 2004 09:27:24 +0200 | |
changeset 14976 | 65f572245276 |
parent 14970 | 8159ade98144 |
child 14981 | e73f8140af78 |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
7772 | 2 |
# |
3 |
# $Id$ |
|
9788 | 4 |
# Author: Markus Wenzel, TU Muenchen |
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
7772 | 6 |
# |
7794 | 7 |
# DESCRIPTION: run LaTeX (and related tools) |
7772 | 8 |
|
9 |
||
10511 | 10 |
PRG="$(basename "$0")" |
7772 | 11 |
|
12 |
function usage() |
|
13 |
{ |
|
14 |
echo |
|
7794 | 15 |
echo "Usage: $PRG [OPTIONS] [FILE]" |
7772 | 16 |
echo |
17 |
echo " Options are:" |
|
7815 | 18 |
echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
14921 | 19 |
echo " pdf, bbl, png, sty, syms" |
7772 | 20 |
echo |
7857 | 21 |
echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
22 |
echo " producing the specified output format." |
|
7772 | 23 |
echo |
24 |
exit 1 |
|
25 |
} |
|
26 |
||
27 |
function fail() |
|
28 |
{ |
|
29 |
echo "$1" >&2 |
|
30 |
exit 2 |
|
31 |
} |
|
32 |
||
33 |
||
34 |
## process command line |
|
35 |
||
36 |
# options |
|
37 |
||
38 |
OUTFORMAT=dvi |
|
39 |
||
40 |
while getopts "o:" OPT |
|
41 |
do |
|
42 |
case "$OPT" in |
|
43 |
o) |
|
44 |
OUTFORMAT="$OPTARG" |
|
45 |
;; |
|
46 |
\?) |
|
47 |
usage |
|
48 |
;; |
|
49 |
esac |
|
50 |
done |
|
51 |
||
52 |
shift $(($OPTIND - 1)) |
|
53 |
||
54 |
||
55 |
# args |
|
56 |
||
7794 | 57 |
FILE="root.tex" |
9788 | 58 |
[ "$#" -ge 1 ] && { FILE="$1"; shift; } |
7772 | 59 |
|
9788 | 60 |
[ "$#" -ne 0 ] && usage |
7772 | 61 |
|
62 |
||
63 |
## main |
|
64 |
||
8564 | 65 |
# root file |
7815 | 66 |
|
7772 | 67 |
DIR=$(dirname "$FILE") |
9788 | 68 |
FILEBASE=$(basename "$FILE" .tex) |
69 |
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" |
|
7772 | 70 |
|
8568 | 71 |
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
7794 | 72 |
|
7815 | 73 |
|
74 |
# operations |
|
75 |
||
14921 | 76 |
#set by configure |
77 |
AUTO_PERL=perl |
|
78 |
||
7815 | 79 |
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
80 |
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
|
81 |
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
|
14344 | 82 |
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
11845 | 83 |
function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
7865 | 84 |
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
12846
0fce95478e19
copy_styles replaces overly conservative update_styles;
wenzelm
parents:
11845
diff
changeset
|
85 |
function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; } |
7815 | 86 |
|
14921 | 87 |
function extract_syms () |
88 |
{ |
|
89 |
"$AUTO_PERL" -n \ |
|
14970
8159ade98144
more generous treatment of packages in draft prints;
wenzelm
parents:
14921
diff
changeset
|
90 |
-e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ |
14921 | 91 |
"$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" |
92 |
"$AUTO_PERL" -n \ |
|
93 |
-e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \ |
|
94 |
"$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" |
|
95 |
} |
|
96 |
||
7772 | 97 |
case "$OUTFORMAT" in |
98 |
dvi) |
|
8564 | 99 |
check_root && \ |
7815 | 100 |
run_latex |
9788 | 101 |
RC="$?" |
7772 | 102 |
;; |
103 |
dvi.gz) |
|
8564 | 104 |
check_root && \ |
7815 | 105 |
run_latex && \ |
7772 | 106 |
gzip -f "$FILEBASE.dvi" |
9788 | 107 |
RC="$?" |
7772 | 108 |
;; |
109 |
ps) |
|
8564 | 110 |
check_root && \ |
7815 | 111 |
run_latex && \ |
112 |
run_dvips && |
|
9788 | 113 |
RC="$?" |
7772 | 114 |
;; |
115 |
ps.gz) |
|
8564 | 116 |
check_root && \ |
7815 | 117 |
run_latex && \ |
118 |
run_dvips && |
|
7772 | 119 |
gzip -f "$FILEBASE.ps" |
9788 | 120 |
RC="$?" |
7772 | 121 |
;; |
122 |
pdf) |
|
8564 | 123 |
check_root && \ |
7815 | 124 |
run_pdflatex |
9788 | 125 |
RC="$?" |
7815 | 126 |
;; |
127 |
bbl) |
|
8564 | 128 |
check_root && \ |
7815 | 129 |
run_bibtex |
9788 | 130 |
RC="$?" |
7772 | 131 |
;; |
14344 | 132 |
idx) |
133 |
check_root && \ |
|
134 |
run_makeindex |
|
135 |
RC="$?" |
|
136 |
;; |
|
7865 | 137 |
png) |
8564 | 138 |
check_root && \ |
7865 | 139 |
run_thumbpdf |
9788 | 140 |
RC="$?" |
7865 | 141 |
;; |
8564 | 142 |
sty) |
12846
0fce95478e19
copy_styles replaces overly conservative update_styles;
wenzelm
parents:
11845
diff
changeset
|
143 |
copy_styles |
9788 | 144 |
RC="$?" |
8564 | 145 |
;; |
14921 | 146 |
syms) |
147 |
extract_syms |
|
148 |
RC="$?" |
|
149 |
;; |
|
7772 | 150 |
*) |
151 |
fail "Bad output format '$OUTFORMAT'" |
|
152 |
;; |
|
153 |
esac |
|
7794 | 154 |
|
9788 | 155 |
exit "$RC" |