1 theory Presentation |
1 theory Presentation |
2 imports Base |
2 imports Base |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Presenting theories \label{ch:present} *} |
5 chapter \<open>Presenting theories \label{ch:present}\<close> |
6 |
6 |
7 text {* Isabelle provides several ways to present the outcome of |
7 text \<open>Isabelle provides several ways to present the outcome of |
8 formal developments, including WWW-based browsable libraries or |
8 formal developments, including WWW-based browsable libraries or |
9 actual printable documents. Presentation is centered around the |
9 actual printable documents. Presentation is centered around the |
10 concept of \emph{sessions} (\chref{ch:session}). The global session |
10 concept of \emph{sessions} (\chref{ch:session}). The global session |
11 structure is that of a tree, with Isabelle Pure at its root, further |
11 structure is that of a tree, with Isabelle Pure at its root, further |
12 object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and |
12 object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and |
43 |
43 |
44 \end{tabular} |
44 \end{tabular} |
45 \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
45 \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
46 \end{center} |
46 \end{center} |
47 \end{figure} |
47 \end{figure} |
48 *} |
48 \<close> |
49 |
49 |
50 |
50 |
51 section {* Generating theory browser information \label{sec:info} *} |
51 section \<open>Generating theory browser information \label{sec:info}\<close> |
52 |
52 |
53 text {* |
53 text \<open> |
54 \index{theory browsing information|bold} |
54 \index{theory browsing information|bold} |
55 |
55 |
56 As a side-effect of building sessions, Isabelle is able to generate |
56 As a side-effect of building sessions, Isabelle is able to generate |
57 theory browsing information, including HTML documents that show the |
57 theory browsing information, including HTML documents that show the |
58 theory sources and the relationship with its ancestors and |
58 theory sources and the relationship with its ancestors and |
101 \bigskip The theory browsing information is stored in a |
101 \bigskip The theory browsing information is stored in a |
102 sub-directory directory determined by the @{setting_ref |
102 sub-directory directory determined by the @{setting_ref |
103 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
103 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
104 session chapter and identifier. In order to present Isabelle |
104 session chapter and identifier. In order to present Isabelle |
105 applications on the web, the corresponding subdirectory from |
105 applications on the web, the corresponding subdirectory from |
106 @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server. *} |
106 @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.\<close> |
107 |
107 |
108 section {* Preparing session root directories \label{sec:tool-mkroot} *} |
108 section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close> |
109 |
109 |
110 text {* The @{tool_def mkroot} tool configures a given directory as |
110 text \<open>The @{tool_def mkroot} tool configures a given directory as |
111 session root, with some @{verbatim ROOT} file and optional document |
111 session root, with some @{verbatim ROOT} file and optional document |
112 source directory. Its usage is: |
112 source directory. Its usage is: |
113 \begin{ttbox} |
113 \begin{ttbox} |
114 Usage: isabelle mkroot [OPTIONS] [DIR] |
114 Usage: isabelle mkroot [OPTIONS] [DIR] |
115 |
115 |
135 name; otherwise the base name of the given directory is used. |
135 name; otherwise the base name of the given directory is used. |
136 |
136 |
137 \medskip The implicit Isabelle settings variable @{setting |
137 \medskip The implicit Isabelle settings variable @{setting |
138 ISABELLE_LOGIC} specifies the parent session, and @{setting |
138 ISABELLE_LOGIC} specifies the parent session, and @{setting |
139 ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
139 ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
140 into the generated @{verbatim ROOT} file. *} |
140 into the generated @{verbatim ROOT} file.\<close> |
141 |
141 |
142 |
142 |
143 subsubsection {* Examples *} |
143 subsubsection \<open>Examples\<close> |
144 |
144 |
145 text {* Produce session @{verbatim Test} (with document preparation) |
145 text \<open>Produce session @{verbatim Test} (with document preparation) |
146 within a separate directory of the same name: |
146 within a separate directory of the same name: |
147 \begin{ttbox} |
147 \begin{ttbox} |
148 isabelle mkroot -d Test && isabelle build -D Test |
148 isabelle mkroot -d Test && isabelle build -D Test |
149 \end{ttbox} |
149 \end{ttbox} |
150 |
150 |
151 \medskip Upgrade the current directory into a session ROOT with |
151 \medskip Upgrade the current directory into a session ROOT with |
152 document preparation, and build it: |
152 document preparation, and build it: |
153 \begin{ttbox} |
153 \begin{ttbox} |
154 isabelle mkroot -d && isabelle build -D . |
154 isabelle mkroot -d && isabelle build -D . |
155 \end{ttbox} |
155 \end{ttbox} |
156 *} |
156 \<close> |
157 |
157 |
158 |
158 |
159 section {* Preparing Isabelle session documents |
159 section \<open>Preparing Isabelle session documents |
160 \label{sec:tool-document} *} |
160 \label{sec:tool-document}\<close> |
161 |
161 |
162 text {* The @{tool_def document} tool prepares logic session |
162 text \<open>The @{tool_def document} tool prepares logic session |
163 documents, processing the sources 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 |
261 deleted after successful run of {\LaTeX} and friends. |
261 deleted after successful run of {\LaTeX} and friends. |
262 |
262 |
263 Some care is needed if the document output location is configured |
263 Some care is needed if the document output location is configured |
264 differently, say within a directory whose content is still required |
264 differently, say within a directory whose content is still required |
265 afterwards! |
265 afterwards! |
266 *} |
266 \<close> |
267 |
267 |
268 |
268 |
269 section {* Running {\LaTeX} within the Isabelle environment |
269 section \<open>Running {\LaTeX} within the Isabelle environment |
270 \label{sec:tool-latex} *} |
270 \label{sec:tool-latex}\<close> |
271 |
271 |
272 text {* The @{tool_def latex} tool provides the basic interface for |
272 text \<open>The @{tool_def latex} tool provides the basic interface for |
273 Isabelle document preparation. Its usage is: |
273 Isabelle document preparation. Its usage is: |
274 \begin{ttbox} |
274 \begin{ttbox} |
275 Usage: isabelle latex [OPTIONS] [FILE] |
275 Usage: isabelle latex [OPTIONS] [FILE] |
276 |
276 |
277 Options are: |
277 Options are: |
295 time by separate tools. |
295 time by separate tools. |
296 |
296 |
297 The @{verbatim syms} output is for internal use; it generates lists |
297 The @{verbatim syms} output is for internal use; it generates lists |
298 of symbols that are available without loading additional {\LaTeX} |
298 of symbols that are available without loading additional {\LaTeX} |
299 packages. |
299 packages. |
300 *} |
300 \<close> |
301 |
301 |
302 |
302 |
303 subsubsection {* Examples *} |
303 subsubsection \<open>Examples\<close> |
304 |
304 |
305 text {* Invoking @{tool latex} by hand may be occasionally useful when |
305 text \<open>Invoking @{tool latex} by hand may be occasionally useful when |
306 debugging failed attempts of the automatic document preparation |
306 debugging failed attempts of the automatic document preparation |
307 stage of batch-mode Isabelle. The abortive process leaves the |
307 stage of batch-mode Isabelle. The abortive process leaves the |
308 sources at a certain place within @{setting ISABELLE_BROWSER_INFO}, |
308 sources at a certain place within @{setting ISABELLE_BROWSER_INFO}, |
309 see the runtime error message for details. This enables users to |
309 see the runtime error message for details. This enables users to |
310 inspect {\LaTeX} runs in further detail, e.g.\ like this: |
310 inspect {\LaTeX} runs in further detail, e.g.\ like this: |
311 |
311 |
312 \begin{ttbox} |
312 \begin{ttbox} |
313 cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document" |
313 cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document" |
314 isabelle latex -o pdf |
314 isabelle latex -o pdf |
315 \end{ttbox} |
315 \end{ttbox} |
316 *} |
316 \<close> |
317 |
317 |
318 end |
318 end |