577 Appendix~\ref{app:symbols} for a complete list of predefined Isabelle |
577 Appendix~\ref{app:symbols} for a complete list of predefined Isabelle |
578 symbols). Users may invent further symbols as well, just by providing |
578 symbols). Users may invent further symbols as well, just by providing |
579 {\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the |
579 {\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the |
580 distribution. |
580 distribution. |
581 |
581 |
582 For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail |
582 For proper setup of PDF documents (with hyperlinks and bookmarks), we |
583 images), we recommend to include \verb,pdfsetup.sty, as well. It is safe to |
583 recommend to include \verb,pdfsetup.sty, as well. It is safe to do so |
584 do so even without using PDF~\LaTeX. |
584 even without using PDF~\LaTeX. |
585 |
585 |
586 \medskip As a final step of document preparation within Isabelle, |
586 \medskip As a final step of document preparation within Isabelle, |
587 \texttt{isatool document -c} is run on the resulting \texttt{document} |
587 \texttt{isatool document -c} is run on the resulting \texttt{document} |
588 directory. Thus the actual output document is built and installed in its |
588 directory. Thus the actual output document is built and installed in its |
589 proper place (as linked by the session's \texttt{index.html} if option |
589 proper place (as linked by the session's \texttt{index.html} if option |
602 \begin{ttbox} |
602 \begin{ttbox} |
603 Usage: latex [OPTIONS] [FILE] |
603 Usage: latex [OPTIONS] [FILE] |
604 |
604 |
605 Options are: |
605 Options are: |
606 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
606 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
607 ps.gz, pdf, bbl, png, sty, syms |
607 ps.gz, pdf, bbl, idx, sty, syms |
608 |
608 |
609 Run LaTeX (and related tools) on FILE (default root.tex), |
609 Run LaTeX (and related tools) on FILE (default root.tex), |
610 producing the specified output format. |
610 producing the specified output format. |
611 \end{ttbox} |
611 \end{ttbox} |
612 Appropriate {\LaTeX}-related programs are run on the input file, according to |
612 Appropriate {\LaTeX}-related programs are run on the input file, |
613 the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips}, |
613 according to the given output format: \texttt{latex}, |
614 \texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}). |
614 \texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}), |
615 The actual commands are determined from the settings environment |
615 and \texttt{makeindex} (for \texttt{idx}). The actual commands are |
616 (\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}). |
616 determined from the settings environment (\texttt{ISABELLE_LATEX} |
|
617 etc., see \S\ref{sec:settings}). |
617 |
618 |
618 The \texttt{sty} output format causes the Isabelle style files to be updated |
619 The \texttt{sty} output format causes the Isabelle style files to be updated |
619 from the distribution. This is useful in special situations where the |
620 from the distribution. This is useful in special situations where the |
620 document sources are to be processed another time by separate tools (cf.\ |
621 document sources are to be processed another time by separate tools (cf.\ |
621 option \texttt{-D} of the \texttt{usedir} utility, see |
622 option \texttt{-D} of the \texttt{usedir} utility, see |