# HG changeset patch
# User wenzelm
# Date 1374957486 -7200
# Node ID 2130b5c4b2873d43fed8814404d9e8a6cb24828d
# Parent  eec610972763f3bb454d5183bdc9c7f944d92542
tuned;

diff -r eec610972763 -r 2130b5c4b287 lib/Tools/document
--- 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