--- a/lib/Tools/document Sat Jul 27 22:20:25 2013 +0200
+++ b/lib/Tools/document Sat Jul 27 22:38:06 2013 +0200
@@ -117,17 +117,6 @@
# prepare document
-function pre_latex ()
-{
- local FMT="$1"
- [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
- "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
- "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" && \
- { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
- { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
- "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex"
-}
-
(
cd "$DIR" || fail "Bad directory '$DIR'"
@@ -138,12 +127,13 @@
if [ -f build ]; then
./build "$OUTFORMAT" "$NAME"
RC="$?"
- elif [ "$OUTFORMAT" = pdf ]; then
- pre_latex pdf && \
- "$ISABELLE_TOOL" latex -o pdf "$ROOT_NAME.tex"
- RC="$?"
else
- pre_latex dvi && \
+ [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
+ "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
+ "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+ { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
+ { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
+ "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
"$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
RC="$?"
fi