125 is conservative in the sense that it does not overwrite existing |
125 is conservative in the sense that it does not overwrite existing |
126 files or directories. Earlier attempts to generate a session root |
126 files or directories. Earlier attempts to generate a session root |
127 need to be deleted manually. |
127 need to be deleted manually. |
128 |
128 |
129 \medskip Option @{verbatim "-d"} indicates that the session shall be |
129 \medskip Option @{verbatim "-d"} indicates that the session shall be |
130 accompanied by a formal document, with @{text dir}@{verbatim |
130 accompanied by a formal document, with @{text DIR}@{verbatim |
131 "/document/root.tex"} as its {\LaTeX} entry point (see also |
131 "/document/root.tex"} as its {\LaTeX} entry point (see also |
132 \chref{ch:present}). |
132 \chref{ch:present}). |
133 |
133 |
134 Option @{verbatim "-n"} allows to specify an alternative session |
134 Option @{verbatim "-n"} allows to specify an alternative session |
135 name; otherwise the base name of the given directory is used. |
135 name; otherwise the base name of the given directory is used. |
158 |
158 |
159 section {* Preparing Isabelle session documents |
159 section {* Preparing Isabelle session documents |
160 \label{sec:tool-document} *} |
160 \label{sec:tool-document} *} |
161 |
161 |
162 text {* The @{tool_def document} tool prepares logic session |
162 text {* The @{tool_def document} tool prepares logic session |
163 documents, processing the sources both as provided by the user and |
163 documents, processing the sources as provided by the user and |
164 generated by Isabelle. Its usage is: |
164 generated by Isabelle. Its usage is: |
165 \begin{ttbox} |
165 \begin{ttbox} |
166 Usage: isabelle document [OPTIONS] [DIR] |
166 Usage: isabelle document [OPTIONS] [DIR] |
167 |
167 |
168 Options are: |
168 Options are: |
218 In more complex situations, a separate @{verbatim build} script for |
218 In more complex situations, a separate @{verbatim build} script for |
219 the document sources may be given. It is invoked with command-line |
219 the document sources may be given. It is invoked with command-line |
220 arguments for the document format and the document variant name. |
220 arguments for the document format and the document variant name. |
221 The script needs to produce corresponding output files, e.g.\ |
221 The script needs to produce corresponding output files, e.g.\ |
222 @{verbatim root.pdf} for target format @{verbatim pdf} (and default |
222 @{verbatim root.pdf} for target format @{verbatim pdf} (and default |
223 default variants). The main work can be again delegated to @{tool |
223 variants). The main work can be again delegated to @{tool latex}, |
224 latex}, but it is also possible to harvest generated {\LaTeX} |
224 but it is also possible to harvest generated {\LaTeX} sources and |
225 sources and copy them elsewhere, for example. |
225 copy them elsewhere. |
226 |
226 |
227 \medskip When running the session, Isabelle copies the content of |
227 \medskip When running the session, Isabelle copies the content of |
228 the original @{verbatim document} directory into its proper place |
228 the original @{verbatim document} directory into its proper place |
229 within @{setting ISABELLE_BROWSER_INFO}, according to the session |
229 within @{setting ISABELLE_BROWSER_INFO}, according to the session |
230 path and document variant. Then, for any processed theory @{text A} |
230 path and document variant. Then, for any processed theory @{text A} |
247 "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim |
247 "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim |
248 "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a |
248 "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a |
249 complete list of predefined Isabelle symbols. Users may invent |
249 complete list of predefined Isabelle symbols. Users may invent |
250 further symbols as well, just by providing {\LaTeX} macros in a |
250 further symbols as well, just by providing {\LaTeX} macros in a |
251 similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of |
251 similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of |
252 the distribution. |
252 the Isabelle distribution. |
253 |
253 |
254 For proper setup of DVI and PDF documents (with hyperlinks and |
254 For proper setup of DVI and PDF documents (with hyperlinks and |
255 bookmarks), we recommend to include @{file |
255 bookmarks), we recommend to include @{file |
256 "~~/lib/texinputs/pdfsetup.sty"} as well. |
256 "~~/lib/texinputs/pdfsetup.sty"} as well. |
257 |
257 |