# HG changeset patch
# User wenzelm
# Date 939906854 -7200
# Node ID 0cb6508f190c9605ef6c9696b73995aa6231428e
# Parent  2efb66472812fe10811221d02100a7881f3e7aed
support thumbpdf;

diff -r 2efb66472812 -r 0cb6508f190c doc-src/System/present.tex
--- a/doc-src/System/present.tex	Thu Oct 14 15:05:35 1999 +0200
+++ b/doc-src/System/present.tex	Thu Oct 14 15:14:14 1999 +0200
@@ -305,15 +305,16 @@
 
   Options are:
     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf, or bbl
+                 ps.gz, pdf, bbl, png
 
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.
 \end{ttbox}
 Appropriate {\LaTeX}-related programs are run on the input file, according to
-the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{bibtex},
-\texttt{dvips}.  The actual commands are determined from the settings
-environment (see \texttt{ISABELLE_LATEX} etc.).
+the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
+\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
+The actual commands are determined from the settings environment
+(\texttt{ISABELLE_LATEX} etc.).
 
 It is important to note that the {\LaTeX} inputs file space has to be properly
 setup to include the Isabelle styles.  Usually, this may be done by modifying
diff -r 2efb66472812 -r 0cb6508f190c lib/texinputs/pdfsetup.sty
--- a/lib/texinputs/pdfsetup.sty	Thu Oct 14 15:05:35 1999 +0200
+++ b/lib/texinputs/pdfsetup.sty	Thu Oct 14 15:14:14 1999 +0200
@@ -5,4 +5,5 @@
 %%
 
 \@ifundefined{pdfoutput}{\usepackage{url}}
-{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}}
+{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}
+  \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}