#!/bin/bash
#
# $Id$
#
# DESCRIPTION: run LaTeX (and related tools)
PRG=$(basename $0)
function usage()
{
echo
echo "Usage: $PRG [OPTIONS] [FILE]"
echo
echo " Options are:"
echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz,"
echo " pdf, bbl, png, sty"
echo
echo " Run LaTeX (and related tools) on FILE (default root.tex),"
echo " producing the specified output format."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
OUTFORMAT=dvi
while getopts "o:" OPT
do
case "$OPT" in
o)
OUTFORMAT="$OPTARG"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
FILE="root.tex"
[ $# -ge 1 ] && { FILE="$1"; shift; }
[ $# -ne 0 ] && usage
## main
# root file
DIR=$(dirname "$FILE")
if [ "$DIR" = . ]; then
FILEBASE=$(basename "$FILE" .tex)
else
FILEBASE=$DIR/$(basename "$FILE" .tex)
fi
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
# operations
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
function update_styles ()
{
for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
do
BNAME=$(basename "$NAME")
if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then
echo "updating $BNAME"
cp -f "$NAME" "$BNAME"
fi
done
}
case "$OUTFORMAT" in
dvi)
check_root && \
run_latex
RC=$?
;;
dvi.gz)
check_root && \
run_latex && \
gzip -f "$FILEBASE.dvi"
RC=$?
;;
ps)
check_root && \
run_latex && \
run_dvips &&
RC=$?
;;
ps.gz)
check_root && \
run_latex && \
run_dvips &&
gzip -f "$FILEBASE.ps"
RC=$?
;;
pdf)
check_root && \
run_pdflatex
RC=$?
;;
bbl)
check_root && \
run_bibtex
RC=$?
;;
png)
check_root && \
run_thumbpdf
RC=$?
;;
sty)
update_styles
RC=$?
;;
*)
fail "Bad output format '$OUTFORMAT'"
;;
esac
exit $RC