diff -r ef6d84f16592 -r cd0fe98db185 lib/Tools/latex
--- a/lib/Tools/latex	Sat Oct 09 23:16:31 1999 +0200
+++ b/lib/Tools/latex	Sat Oct 09 23:16:59 1999 +0200
@@ -13,7 +13,8 @@
   echo "Usage: $PRG [OPTIONS] [FILE]"
   echo
   echo "  Options are:"
-  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
+  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
+  echo "                 pdf, or bbl"
   echo
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex), producing the"
@@ -60,6 +61,8 @@
 
 ## main
 
+# check file
+
 DIR=$(dirname "$FILE")
 if [ "$DIR" = . ]; then
   FILEBASE=$(basename "$FILE" .tex)
@@ -69,29 +72,44 @@
 
 [ -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"; }
+
+
+# process file
+
 case "$OUTFORMAT" in
   dvi)
-    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    run_latex
     RC=$?
     ;;
   dvi.gz)
-    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" && \
+    run_latex && \
     gzip -f "$FILEBASE.dvi"
     RC=$?
     ;;
   ps)
-    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" && \
-    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
+    run_latex && \
+    run_dvips &&
     RC=$?
     ;;
   ps.gz)
-    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" && \
-    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi" && \
+    run_latex && \
+    run_dvips &&
     gzip -f "$FILEBASE.ps"
     RC=$?
     ;;
   pdf)
-    $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    run_pdflatex
+    RC=$?
+    ;;
+  bbl)
+    run_bibtex
     RC=$?
     ;;
   *)