# HG changeset patch
# User wenzelm
# Date 939906214 -7200
# Node ID d9be8bc5624e6f1af18a8e0c5cfa2fed1ab90baa
# Parent  5cd5a27f5c9380e62f013c711d96dc77672c9c25
support thumbpdf (via 'png' output format);

diff -r 5cd5a27f5c93 -r d9be8bc5624e lib/Tools/latex
--- a/lib/Tools/latex	Thu Oct 14 15:02:04 1999 +0200
+++ b/lib/Tools/latex	Thu Oct 14 15:03:34 1999 +0200
@@ -14,7 +14,7 @@
   echo
   echo "  Options are:"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
-  echo "                 pdf, or bbl"
+  echo "                 pdf, bbl, png"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
@@ -78,6 +78,7 @@
 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"; }
 
 
 # process file
@@ -111,6 +112,10 @@
     run_bibtex
     RC=$?
     ;;
+  png)
+    run_thumbpdf
+    RC=$?
+    ;;
   *)
     fail "Bad output format '$OUTFORMAT'"
     ;;