author | wenzelm |
Fri, 01 Sep 2000 17:50:36 +0200 | |
changeset 9788 | df671fa2562a |
parent 8568 | b18540435f26 |
child 10511 | efb3428c9879 |
permissions | -rwxr-xr-x |
wenzelm@7772 | 1 |
#!/bin/bash |
wenzelm@7772 | 2 |
# |
wenzelm@7772 | 3 |
# $Id$ |
wenzelm@9788 | 4 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9788 | 5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@7772 | 6 |
# |
wenzelm@7794 | 7 |
# DESCRIPTION: run LaTeX (and related tools) |
wenzelm@7772 | 8 |
|
wenzelm@7772 | 9 |
|
wenzelm@9788 | 10 |
PRG=$(basename "$0") |
wenzelm@7772 | 11 |
|
wenzelm@7772 | 12 |
function usage() |
wenzelm@7772 | 13 |
{ |
wenzelm@7772 | 14 |
echo |
wenzelm@7794 | 15 |
echo "Usage: $PRG [OPTIONS] [FILE]" |
wenzelm@7772 | 16 |
echo |
wenzelm@7772 | 17 |
echo " Options are:" |
wenzelm@7815 | 18 |
echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
wenzelm@8564 | 19 |
echo " pdf, bbl, png, sty" |
wenzelm@7772 | 20 |
echo |
wenzelm@7857 | 21 |
echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
wenzelm@7857 | 22 |
echo " producing the specified output format." |
wenzelm@7772 | 23 |
echo |
wenzelm@7772 | 24 |
exit 1 |
wenzelm@7772 | 25 |
} |
wenzelm@7772 | 26 |
|
wenzelm@7772 | 27 |
function fail() |
wenzelm@7772 | 28 |
{ |
wenzelm@7772 | 29 |
echo "$1" >&2 |
wenzelm@7772 | 30 |
exit 2 |
wenzelm@7772 | 31 |
} |
wenzelm@7772 | 32 |
|
wenzelm@7772 | 33 |
|
wenzelm@7772 | 34 |
## process command line |
wenzelm@7772 | 35 |
|
wenzelm@7772 | 36 |
# options |
wenzelm@7772 | 37 |
|
wenzelm@7772 | 38 |
OUTFORMAT=dvi |
wenzelm@7772 | 39 |
|
wenzelm@7772 | 40 |
while getopts "o:" OPT |
wenzelm@7772 | 41 |
do |
wenzelm@7772 | 42 |
case "$OPT" in |
wenzelm@7772 | 43 |
o) |
wenzelm@7772 | 44 |
OUTFORMAT="$OPTARG" |
wenzelm@7772 | 45 |
;; |
wenzelm@7772 | 46 |
\?) |
wenzelm@7772 | 47 |
usage |
wenzelm@7772 | 48 |
;; |
wenzelm@7772 | 49 |
esac |
wenzelm@7772 | 50 |
done |
wenzelm@7772 | 51 |
|
wenzelm@7772 | 52 |
shift $(($OPTIND - 1)) |
wenzelm@7772 | 53 |
|
wenzelm@7772 | 54 |
|
wenzelm@7772 | 55 |
# args |
wenzelm@7772 | 56 |
|
wenzelm@7794 | 57 |
FILE="root.tex" |
wenzelm@9788 | 58 |
[ "$#" -ge 1 ] && { FILE="$1"; shift; } |
wenzelm@7772 | 59 |
|
wenzelm@9788 | 60 |
[ "$#" -ne 0 ] && usage |
wenzelm@7772 | 61 |
|
wenzelm@7772 | 62 |
|
wenzelm@7772 | 63 |
## main |
wenzelm@7772 | 64 |
|
wenzelm@8564 | 65 |
# root file |
wenzelm@7815 | 66 |
|
wenzelm@7772 | 67 |
DIR=$(dirname "$FILE") |
wenzelm@9788 | 68 |
FILEBASE=$(basename "$FILE" .tex) |
wenzelm@9788 | 69 |
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" |
wenzelm@7772 | 70 |
|
wenzelm@8568 | 71 |
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
wenzelm@7794 | 72 |
|
wenzelm@7815 | 73 |
|
wenzelm@7815 | 74 |
# operations |
wenzelm@7815 | 75 |
|
wenzelm@7815 | 76 |
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
wenzelm@7815 | 77 |
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
wenzelm@7815 | 78 |
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
wenzelm@7815 | 79 |
function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
wenzelm@7865 | 80 |
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
wenzelm@7815 | 81 |
|
wenzelm@8564 | 82 |
function update_styles () |
wenzelm@8564 | 83 |
{ |
wenzelm@9788 | 84 |
for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty |
wenzelm@8564 | 85 |
do |
wenzelm@8565 | 86 |
DEST="$DIR"/$(basename "$NAME") |
wenzelm@8565 | 87 |
if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then |
wenzelm@8565 | 88 |
echo "updating $DEST" |
wenzelm@8565 | 89 |
cp -f "$NAME" "$DEST" |
wenzelm@8564 | 90 |
fi |
wenzelm@8564 | 91 |
done |
wenzelm@8564 | 92 |
} |
wenzelm@7815 | 93 |
|
wenzelm@7772 | 94 |
case "$OUTFORMAT" in |
wenzelm@7772 | 95 |
dvi) |
wenzelm@8564 | 96 |
check_root && \ |
wenzelm@7815 | 97 |
run_latex |
wenzelm@9788 | 98 |
RC="$?" |
wenzelm@7772 | 99 |
;; |
wenzelm@7772 | 100 |
dvi.gz) |
wenzelm@8564 | 101 |
check_root && \ |
wenzelm@7815 | 102 |
run_latex && \ |
wenzelm@7772 | 103 |
gzip -f "$FILEBASE.dvi" |
wenzelm@9788 | 104 |
RC="$?" |
wenzelm@7772 | 105 |
;; |
wenzelm@7772 | 106 |
ps) |
wenzelm@8564 | 107 |
check_root && \ |
wenzelm@7815 | 108 |
run_latex && \ |
wenzelm@7815 | 109 |
run_dvips && |
wenzelm@9788 | 110 |
RC="$?" |
wenzelm@7772 | 111 |
;; |
wenzelm@7772 | 112 |
ps.gz) |
wenzelm@8564 | 113 |
check_root && \ |
wenzelm@7815 | 114 |
run_latex && \ |
wenzelm@7815 | 115 |
run_dvips && |
wenzelm@7772 | 116 |
gzip -f "$FILEBASE.ps" |
wenzelm@9788 | 117 |
RC="$?" |
wenzelm@7772 | 118 |
;; |
wenzelm@7772 | 119 |
pdf) |
wenzelm@8564 | 120 |
check_root && \ |
wenzelm@7815 | 121 |
run_pdflatex |
wenzelm@9788 | 122 |
RC="$?" |
wenzelm@7815 | 123 |
;; |
wenzelm@7815 | 124 |
bbl) |
wenzelm@8564 | 125 |
check_root && \ |
wenzelm@7815 | 126 |
run_bibtex |
wenzelm@9788 | 127 |
RC="$?" |
wenzelm@7772 | 128 |
;; |
wenzelm@7865 | 129 |
png) |
wenzelm@8564 | 130 |
check_root && \ |
wenzelm@7865 | 131 |
run_thumbpdf |
wenzelm@9788 | 132 |
RC="$?" |
wenzelm@7865 | 133 |
;; |
wenzelm@8564 | 134 |
sty) |
wenzelm@8564 | 135 |
update_styles |
wenzelm@9788 | 136 |
RC="$?" |
wenzelm@8564 | 137 |
;; |
wenzelm@7772 | 138 |
*) |
wenzelm@7772 | 139 |
fail "Bad output format '$OUTFORMAT'" |
wenzelm@7772 | 140 |
;; |
wenzelm@7772 | 141 |
esac |
wenzelm@7794 | 142 |
|
wenzelm@9788 | 143 |
exit "$RC" |