author | nipkow |
Tue, 05 Nov 2019 14:57:41 +0100 | |
changeset 71033 | c1b63124245c |
parent 67399 | eab6ce8368fa |
child 72309 | 564012e31db1 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
28221 | 3 |
theory Presentation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42009
diff
changeset
|
4 |
imports Base |
28221 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>Presenting theories \label{ch:present}\<close> |
28221 | 8 |
|
61575 | 9 |
text \<open> |
10 |
Isabelle provides several ways to present the outcome of formal |
|
11 |
developments, including WWW-based browsable libraries or actual printable |
|
12 |
documents. Presentation is centered around the concept of \<^emph>\<open>sessions\<close> |
|
13 |
(\chref{ch:session}). The global session structure is that of a tree, with |
|
14 |
Isabelle Pure at its root, further object-logics derived (e.g.\ HOLCF from |
|
15 |
HOL, and HOL from Pure), and application sessions further on in the |
|
16 |
hierarchy. |
|
28221 | 17 |
|
61575 | 18 |
The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means |
19 |
for managing Isabelle sessions, including proper setup for presentation; |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62013
diff
changeset
|
20 |
@{tool build} tells the Isabelle process to run any additional stages |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62013
diff
changeset
|
21 |
required for document preparation, notably the @{tool_ref document} and |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62013
diff
changeset
|
22 |
@{tool_ref latex}. The complete tool chain for managing batch-mode Isabelle |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62013
diff
changeset
|
23 |
sessions is illustrated in \figref{fig:session-tools}. |
28221 | 24 |
|
25 |
\begin{figure}[htbp] |
|
26 |
\begin{center} |
|
27 |
\begin{tabular}{lp{0.6\textwidth}} |
|
28 |
||
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
29 |
@{tool_ref mkroot} & invoked once by the user to initialize the |
61503 | 30 |
session \<^verbatim>\<open>ROOT\<close> with optional \<^verbatim>\<open>document\<close> |
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
31 |
directory; \\ |
28221 | 32 |
|
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
33 |
@{tool_ref build} & invoked repeatedly by the user to keep |
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
34 |
session output up-to-date (HTML, documents etc.); \\ |
28221 | 35 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62013
diff
changeset
|
36 |
@{tool_ref process} & run through @{tool_ref build}; \\ |
28221 | 37 |
|
48602 | 38 |
@{tool_ref document} & run by the Isabelle process if document |
39 |
preparation is enabled; \\ |
|
28221 | 40 |
|
48602 | 41 |
@{tool_ref latex} & universal {\LaTeX} tool wrapper invoked |
42 |
multiple times by @{tool_ref document}; also useful for manual |
|
43 |
experiments; \\ |
|
28221 | 44 |
|
45 |
\end{tabular} |
|
46 |
\caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
|
47 |
\end{center} |
|
48 |
\end{figure} |
|
58618 | 49 |
\<close> |
28221 | 50 |
|
51 |
||
62013 | 52 |
section \<open>Generating HTML browser information \label{sec:info}\<close> |
28221 | 53 |
|
58618 | 54 |
text \<open> |
61575 | 55 |
As a side-effect of building sessions, Isabelle is able to generate theory |
56 |
browsing information, including HTML documents that show the theory sources |
|
57 |
and the relationship with its ancestors and descendants. Besides the HTML |
|
58 |
file that is generated for every theory, Isabelle stores links to all |
|
59 |
theories of a session in an index file. As a second hierarchy, groups of |
|
60 |
sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the |
|
61 |
implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant |
|
51417 | 62 |
for the presentation. |
28221 | 63 |
|
61406 | 64 |
\<^medskip> |
62013 | 65 |
To generate theory browsing information for an existing session, just invoke |
66 |
@{tool build} with suitable options: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
67 |
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>} |
28221 | 68 |
|
61575 | 69 |
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as |
70 |
reported by the above verbose invocation of the build process. |
|
28221 | 71 |
|
67219 | 72 |
Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in |
73 |
\<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are |
|
74 |
prepared automatically as well if enabled like this: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
75 |
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>} |
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
76 |
|
61575 | 77 |
Enabling both browser info and document preparation simultaneously causes an |
78 |
appropriate ``document'' link to be included in the HTML index. Documents |
|
79 |
may be generated independently of browser information as well, see |
|
80 |
\secref{sec:tool-document} for further details. |
|
28221 | 81 |
|
61406 | 82 |
\<^bigskip> |
61575 | 83 |
The theory browsing information is stored in a sub-directory directory |
84 |
determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix |
|
85 |
corresponding to the session chapter and identifier. In order to present |
|
86 |
Isabelle applications on the web, the corresponding subdirectory from |
|
87 |
@{setting ISABELLE_BROWSER_INFO} can be put on a WWW server. |
|
88 |
\<close> |
|
28221 | 89 |
|
61406 | 90 |
|
58618 | 91 |
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close> |
28221 | 92 |
|
61575 | 93 |
text \<open> |
94 |
The @{tool_def mkroot} tool configures a given directory as session root, |
|
95 |
with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
96 |
@{verbatim [display] |
67043 | 97 |
\<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY] |
28221 | 98 |
|
99 |
Options are: |
|
67043 | 100 |
-A LATEX provide author in LaTeX notation (default: user name) |
67069
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
101 |
-I init Mercurial repository and add generated files |
67043 | 102 |
-T LATEX provide title in LaTeX notation (default: session name) |
103 |
-n NAME alternative session name (default: directory base name) |
|
28221 | 104 |
|
67043 | 105 |
Prepare session root directory (default: current directory). |
106 |
\<close>} |
|
28221 | 107 |
|
61575 | 108 |
The results are placed in the given directory \<open>dir\<close>, which refers to the |
109 |
current directory by default. The @{tool mkroot} tool is conservative in the |
|
110 |
sense that it does not overwrite existing files or directories. Earlier |
|
111 |
attempts to generate a session root need to be deleted manually. |
|
28221 | 112 |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
113 |
The generated session template will be accompanied by a formal document, |
67043 | 114 |
with \<open>DIRECTORY\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also |
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
115 |
\chref{ch:present}). |
28221 | 116 |
|
67043 | 117 |
Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly, |
118 |
using {\LaTeX} source notation. |
|
119 |
||
67069
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
120 |
Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and |
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
121 |
adds all generated files (without commit). |
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
122 |
|
67043 | 123 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name |
124 |
of the given directory is used. |
|
28221 | 125 |
|
61406 | 126 |
\<^medskip> |
61575 | 127 |
The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies |
67043 | 128 |
the parent session. |
61503 | 129 |
\<close> |
28221 | 130 |
|
131 |
||
58618 | 132 |
subsubsection \<open>Examples\<close> |
28221 | 133 |
|
61575 | 134 |
text \<open> |
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
135 |
Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name: |
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
136 |
@{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>} |
28221 | 137 |
|
61406 | 138 |
\<^medskip> |
61575 | 139 |
Upgrade the current directory into a session ROOT with document preparation, |
140 |
and build it: |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
141 |
@{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>} |
58618 | 142 |
\<close> |
28221 | 143 |
|
144 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
145 |
section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close> |
28221 | 146 |
|
61575 | 147 |
text \<open> |
148 |
The @{tool_def document} tool prepares logic session documents, processing |
|
149 |
the sources as provided by the user and generated by Isabelle. Its usage is: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
150 |
@{verbatim [display] |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
151 |
\<open>Usage: isabelle document [OPTIONS] |
28221 | 152 |
|
153 |
Options are: |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
154 |
-d DIR document output directory (default "output/document") |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
155 |
-n NAME document name (default "document") |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
156 |
-o FORMAT document format: pdf (default), dvi |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
157 |
-t TAGS markup for tagged regions |
28221 | 158 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
159 |
Prepare the theory session document in document directory, producing the |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
160 |
specified output format. |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
161 |
\<close>} |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
162 |
|
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
163 |
This tool is usually run automatically as part of the Isabelle build |
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
164 |
process, provided document preparation has been enabled via suitable |
61575 | 165 |
options. It may be manually invoked on the generated browser information |
166 |
document output as well, e.g.\ in case of errors encountered in the batch |
|
167 |
run. |
|
28221 | 168 |
|
61406 | 169 |
\<^medskip> |
67351 | 170 |
Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
171 |
is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
172 |
will appear in the parent of this directory. |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
173 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
174 |
\<^medskip> |
61575 | 175 |
The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format, |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
176 |
the default is ``\<^verbatim>\<open>document.pdf\<close>''. |
28221 | 177 |
|
61406 | 178 |
\<^medskip> |
61575 | 179 |
The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command |
180 |
regions. Tags are specified as a comma separated list of modifier/name |
|
181 |
pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to |
|
182 |
drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is |
|
183 |
equivalent to the tag specification |
|
67151 | 184 |
``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>''; |
185 |
see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and |
|
186 |
\<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. |
|
28221 | 187 |
|
61406 | 188 |
\<^medskip> |
61575 | 189 |
Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session |
190 |
sources. This directory is supposed to contain all the files needed to |
|
191 |
produce the final document --- apart from the actual theories which are |
|
192 |
generated by Isabelle. |
|
28221 | 193 |
|
61406 | 194 |
\<^medskip> |
61575 | 195 |
For most practical purposes, @{tool document} is smart enough to create any |
196 |
of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as |
|
197 |
a starting point. This even includes multiple runs of {\LaTeX} to |
|
198 |
accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close> |
|
199 |
within the same directory). |
|
28221 | 200 |
|
61575 | 201 |
In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document |
202 |
sources may be given. It is invoked with command-line arguments for the |
|
203 |
document format and the document variant name. The script needs to produce |
|
204 |
corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and |
|
205 |
default variants). The main work can be again delegated to @{tool latex}, |
|
206 |
but it is also possible to harvest generated {\LaTeX} sources and copy them |
|
207 |
elsewhere. |
|
28221 | 208 |
|
61406 | 209 |
\<^medskip> |
61575 | 210 |
When running the session, Isabelle copies the content of the original |
211 |
\<^verbatim>\<open>document\<close> directory into its proper place within @{setting |
|
212 |
ISABELLE_BROWSER_INFO}, according to the session path and document variant. |
|
213 |
Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put |
|
214 |
there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is |
|
215 |
put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the |
|
216 |
user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the |
|
217 |
theories. |
|
28221 | 218 |
|
63680 | 219 |
The {\LaTeX} versions of the theories require some macros defined in |
220 |
\<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in |
|
61575 | 221 |
\<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an |
222 |
appropriate path specification for {\TeX} inputs. |
|
28221 | 223 |
|
61575 | 224 |
If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then |
225 |
\<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a |
|
226 |
standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to |
|
227 |
\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list |
|
228 |
of predefined Isabelle symbols. Users may invent further symbols as well, |
|
63680 | 229 |
just by providing {\LaTeX} macros in a similar fashion as in |
230 |
\<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution. |
|
28221 | 231 |
|
61575 | 232 |
For proper setup of DVI and PDF documents (with hyperlinks and bookmarks), |
63680 | 233 |
we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well. |
28221 | 234 |
|
61406 | 235 |
\<^medskip> |
67185 | 236 |
As a final step of Isabelle document preparation, @{tool document} is run on |
237 |
the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document |
|
238 |
is built and installed in its proper place. The generated sources are |
|
239 |
deleted after successful run of {\LaTeX} and friends. |
|
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
240 |
|
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
241 |
Some care is needed if the document output location is configured |
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
242 |
differently, say within a directory whose content is still required |
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
243 |
afterwards! |
58618 | 244 |
\<close> |
28221 | 245 |
|
246 |
||
58618 | 247 |
section \<open>Running {\LaTeX} within the Isabelle environment |
248 |
\label{sec:tool-latex}\<close> |
|
28221 | 249 |
|
61575 | 250 |
text \<open> |
251 |
The @{tool_def latex} tool provides the basic interface for Isabelle |
|
252 |
document preparation. Its usage is: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
253 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
254 |
\<open>Usage: isabelle latex [OPTIONS] [FILE] |
28221 | 255 |
|
256 |
Options are: |
|
67263 | 257 |
-o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty |
28221 | 258 |
|
259 |
Run LaTeX (and related tools) on FILE (default root.tex), |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
260 |
producing the specified output format.\<close>} |
28221 | 261 |
|
61575 | 262 |
Appropriate {\LaTeX}-related programs are run on the input file, according |
263 |
to the given output format: @{executable latex}, @{executable pdflatex}, |
|
264 |
@{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable |
|
265 |
makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the |
|
266 |
settings environment (@{setting ISABELLE_PDFLATEX} etc.). |
|
28221 | 267 |
|
61575 | 268 |
The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from |
269 |
the distribution. This is useful in special situations where the document |
|
270 |
sources are to be processed another time by separate tools. |
|
58618 | 271 |
\<close> |
28221 | 272 |
|
273 |
||
58618 | 274 |
subsubsection \<open>Examples\<close> |
28221 | 275 |
|
61575 | 276 |
text \<open> |
277 |
Invoking @{tool latex} by hand may be occasionally useful when debugging |
|
278 |
failed attempts of the automatic document preparation stage of batch-mode |
|
279 |
Isabelle. The abortive process leaves the sources at a certain place within |
|
280 |
@{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details. |
|
281 |
This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like |
|
282 |
this: |
|
48602 | 283 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
284 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
285 |
\<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document" |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
286 |
isabelle latex -o pdf\<close>} |
58618 | 287 |
\<close> |
28221 | 288 |
|
67399 | 289 |
end |