1.1 --- a/doc-src/IsarRef/Thy/intro.thy	Thu May 15 18:12:43 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/intro.thy	Thu May 15 20:02:37 2008 +0200
     1.3 @@ -221,13 +221,10 @@
     1.4  text {*
     1.5    Isabelle/Isar provides a simple document preparation system based on
     1.6    existing {PDF-\LaTeX} technology, with full support of hyper-links
     1.7 -  (both local references and URLs), bookmarks, and thumbnails.  Thus
     1.8 -  the results are equally well suited for WWW browsing and as printed
     1.9 -  copies.
    1.10 +  (both local references and URLs) and bookmarks.  Thus the results
    1.11 +  are equally well suited for WWW browsing and as printed copies.
    1.12  
    1.13 -  \medskip
    1.14 -
    1.15 -  Isabelle generates {\LaTeX} output as part of the run of a
    1.16 +  \medskip Isabelle generates {\LaTeX} output as part of the run of a
    1.17    \emph{logic session} (see also \cite{isabelle-sys}).  Getting
    1.18    started with a working configuration for common situations is quite
    1.19    easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}

     2.1 --- a/doc-src/System/present.tex	Thu May 15 18:12:43 2008 +0200
     2.2 +++ b/doc-src/System/present.tex	Thu May 15 20:02:37 2008 +0200
     2.3 @@ -579,9 +579,9 @@
     2.4  {\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the
     2.5  distribution.
     2.6  
     2.7 -For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
     2.8 -images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
     2.9 -do so even without using PDF~\LaTeX.
    2.10 +For proper setup of PDF documents (with hyperlinks and bookmarks), we
    2.11 +recommend to include \verb,pdfsetup.sty, as well.  It is safe to do so
    2.12 +even without using PDF~\LaTeX.
    2.13  
    2.14  \medskip As a final step of document preparation within Isabelle,
    2.15  \texttt{isatool document -c} is run on the resulting \texttt{document}
    2.16 @@ -604,16 +604,17 @@
    2.17  
    2.18    Options are:
    2.19      -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
    2.20 -                 ps.gz, pdf, bbl, png, sty, syms
    2.21 +                 ps.gz, pdf, bbl, idx, sty, syms
    2.22  
    2.23    Run LaTeX (and related tools) on FILE (default root.tex),
    2.24    producing the specified output format.
    2.25  \end{ttbox}
    2.26 -Appropriate {\LaTeX}-related programs are run on the input file, according to
    2.27 -the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
    2.28 -\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
    2.29 -The actual commands are determined from the settings environment
    2.30 -(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
    2.31 +Appropriate {\LaTeX}-related programs are run on the input file,
    2.32 +according to the given output format: \texttt{latex},
    2.33 +\texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}),
    2.34 +and \texttt{makeindex} (for \texttt{idx}).  The actual commands are
    2.35 +determined from the settings environment (\texttt{ISABELLE_LATEX}
    2.36 +etc., see \S\ref{sec:settings}).
    2.37  
    2.38  The \texttt{sty} output format causes the Isabelle style files to be updated
    2.39  from the distribution.  This is useful in special situations where the

     3.1 --- a/etc/settings	Thu May 15 18:12:43 2008 +0200
     3.2 +++ b/etc/settings	Thu May 15 20:02:37 2008 +0200
     3.3 @@ -116,10 +116,6 @@
     3.4  # Paranoia setting for strange latex installations ...
     3.5  #unset TEXMF
     3.6  
     3.7 -# If ISABELLE_THUMBPDF is set, isatool tries to
     3.8 -# generate thumbnails for proof documents
     3.9 -#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
    3.10 -
    3.11  
    3.12  ###
    3.13  ### Misc path settings

     4.1 --- a/lib/Tools/document	Thu May 15 18:12:43 2008 +0200
     4.2 +++ b/lib/Tools/document	Thu May 15 20:02:37 2008 +0200
     4.3 @@ -139,10 +139,6 @@
     4.4    elif [ "$OUTFORMAT" = pdf ]; then
     4.5      pre_latex pdf && \
     4.6      "$ISATOOL" latex -o pdf && \
     4.7 -    { if [ -n "$ISABELLE_THUMBPDF" ]; then
     4.8 -        "$ISATOOL" latex -o png && \
     4.9 -        "$ISATOOL" latex -o pdf
    4.10 -      fi; }
    4.11      RC="$?"
    4.12    else
    4.13      pre_latex dvi && \

     5.1 --- a/lib/Tools/latex	Thu May 15 18:12:43 2008 +0200
     5.2 +++ b/lib/Tools/latex	Thu May 15 20:02:37 2008 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4    echo
     5.5    echo "  Options are:"
     5.6    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     5.7 -  echo "                 pdf, bbl, png, sty, syms"
     5.8 +  echo "                 pdf, bbl, idx, sty, syms"
     5.9    echo
    5.10    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    5.11    echo "  producing the specified output format."
    5.12 @@ -77,7 +77,6 @@
    5.13  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    5.14  function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    5.15  function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    5.16 -function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    5.17  function copy_styles ()
    5.18  {
    5.19    for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
    5.20 @@ -137,11 +136,6 @@
    5.21      run_makeindex
    5.22      RC="$?"
    5.23      ;;
    5.24 -  png)
    5.25 -    check_root && \
    5.26 -    run_thumbpdf
    5.27 -    RC="$?"
    5.28 -    ;;
    5.29    sty)
    5.30      copy_styles
    5.31      RC="$?"