--- 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}
--- 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
--- 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
--- 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 && \
--- 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="$?"