# HG changeset patch
# User wenzelm
# Date 1210874557 -7200
# Node ID 25fb7241f32e721c02518fe6968bba79054c612d
# Parent  75466ad27dd7a16c9a0c080ddcc3cec88214d9d8
removed obsolete thumbpdf;

diff -r 75466ad27dd7 -r 25fb7241f32e doc-src/IsarRef/Thy/intro.thy
--- a/doc-src/IsarRef/Thy/intro.thy	Thu May 15 18:12:43 2008 +0200
+++ b/doc-src/IsarRef/Thy/intro.thy	Thu May 15 20:02:37 2008 +0200
@@ -221,13 +221,10 @@
 text {*
   Isabelle/Isar provides a simple document preparation system based on
   existing {PDF-\LaTeX} technology, with full support of hyper-links
-  (both local references and URLs), bookmarks, and thumbnails.  Thus
-  the results are equally well suited for WWW browsing and as printed
-  copies.
+  (both local references and URLs) and bookmarks.  Thus the results
+  are equally well suited for WWW browsing and as printed copies.
 
-  \medskip
-
-  Isabelle generates {\LaTeX} output as part of the run of a
+  \medskip Isabelle generates {\LaTeX} output as part of the run of a
   \emph{logic session} (see also \cite{isabelle-sys}).  Getting
   started with a working configuration for common situations is quite
   easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
diff -r 75466ad27dd7 -r 25fb7241f32e doc-src/System/present.tex
--- a/doc-src/System/present.tex	Thu May 15 18:12:43 2008 +0200
+++ b/doc-src/System/present.tex	Thu May 15 20:02:37 2008 +0200
@@ -579,9 +579,9 @@
 {\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the
 distribution.
 
-For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
-images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
-do so even without using PDF~\LaTeX.
+For proper setup of PDF documents (with hyperlinks and bookmarks), we
+recommend to include \verb,pdfsetup.sty, as well.  It is safe to do so
+even without using PDF~\LaTeX.
 
 \medskip As a final step of document preparation within Isabelle,
 \texttt{isatool document -c} is run on the resulting \texttt{document}
@@ -604,16 +604,17 @@
 
   Options are:
     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf, bbl, png, sty, syms
+                 ps.gz, pdf, bbl, idx, sty, syms
 
   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{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., see \S\ref{sec:settings}).
+Appropriate {\LaTeX}-related programs are run on the input file,
+according to the given output format: \texttt{latex},
+\texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}),
+and \texttt{makeindex} (for \texttt{idx}).  The actual commands are
+determined from the settings environment (\texttt{ISABELLE_LATEX}
+etc., see \S\ref{sec:settings}).
 
 The \texttt{sty} output format causes the Isabelle style files to be updated
 from the distribution.  This is useful in special situations where the
diff -r 75466ad27dd7 -r 25fb7241f32e etc/settings
--- a/etc/settings	Thu May 15 18:12:43 2008 +0200
+++ b/etc/settings	Thu May 15 20:02:37 2008 +0200
@@ -116,10 +116,6 @@
 # Paranoia setting for strange latex installations ...
 #unset TEXMF
 
-# If ISABELLE_THUMBPDF is set, isatool tries to
-# generate thumbnails for proof documents
-#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
-
 
 ###
 ### Misc path settings
diff -r 75466ad27dd7 -r 25fb7241f32e lib/Tools/document
--- a/lib/Tools/document	Thu May 15 18:12:43 2008 +0200
+++ b/lib/Tools/document	Thu May 15 20:02:37 2008 +0200
@@ -139,10 +139,6 @@
   elif [ "$OUTFORMAT" = pdf ]; then
     pre_latex pdf && \
     "$ISATOOL" latex -o pdf && \
-    { if [ -n "$ISABELLE_THUMBPDF" ]; then
-        "$ISATOOL" latex -o png && \
-        "$ISATOOL" latex -o pdf
-      fi; }
     RC="$?"
   else
     pre_latex dvi && \
diff -r 75466ad27dd7 -r 25fb7241f32e lib/Tools/latex
--- a/lib/Tools/latex	Thu May 15 18:12:43 2008 +0200
+++ b/lib/Tools/latex	Thu May 15 20:02:37 2008 +0200
@@ -15,7 +15,7 @@
   echo
   echo "  Options are:"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
-  echo "                 pdf, bbl, png, sty, syms"
+  echo "                 pdf, bbl, idx, sty, syms"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
@@ -77,7 +77,6 @@
 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
-function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
 function copy_styles ()
 {
   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
@@ -137,11 +136,6 @@
     run_makeindex
     RC="$?"
     ;;
-  png)
-    check_root && \
-    run_thumbpdf
-    RC="$?"
-    ;;
   sty)
     copy_styles
     RC="$?"