diff -r 001d10bbc61b -r 16d4b8c09086 doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Sun Jan 06 13:47:55 2002 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Sun Jan 06 13:48:18 2002 +0100 @@ -2,7 +2,7 @@ theory Documents = Main: (*>*) -section {* Concrete syntax \label{sec:concrete-syntax} *} +section {* Concrete Syntax \label{sec:concrete-syntax} *} text {* Concerning Isabelle's ``inner'' language of simply-typed @{text @@ -25,7 +25,7 @@ *} -subsection {* Infix annotations *} +subsection {* Infix Annotations *} text {* Syntax annotations may be included wherever constants are declared @@ -84,7 +84,7 @@ @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In contrast, a \emph{non-oriented} declaration via \isakeyword{infix} would always demand explicit parentheses. - + Many binary operations observe the associative law, so the exact grouping does not matter. Nevertheless, formal statements need be given in a particular format, associativity needs to be treated @@ -106,7 +106,7 @@ *} -subsection {* Mathematical symbols \label{sec:thy-present-symbols} *} +subsection {* Mathematical Symbols \label{sec:thy-present-symbols} *} text {* Concrete syntax based on plain ASCII characters has its inherent @@ -222,7 +222,7 @@ xor :: "bool \ bool \ bool" (infixl "\\" 60) -subsection {* Prefix annotations *} +subsection {* Prefix Annotations *} text {* Prefix syntax annotations\index{prefix annotation} are just a very @@ -264,7 +264,7 @@ currency :: "currency \ nat" ("\") -subsection {* Syntax translations \label{sec:def-translations} *} +subsection {* Syntax Translations \label{sec:def-translations} *} text{* FIXME @@ -291,7 +291,7 @@ parsing or printing. This tutorial will not cover the details of translations. We have mentioned the concept merely because it crops up occasionally; a number of HOL's built-in constructs are defined -via translations. Translations are preferable to definitions when the new +via translations. Translations are preferable to definitions when the new concept is a trivial variation on an existing one. For example, we don't need to derive new theorems about @{text"\"}, since existing theorems about @{text"="} still apply.% @@ -300,7 +300,7 @@ *} -section {* Document preparation *} +section {* Document Preparation *} text {* Isabelle/Isar is centered around a certain notion of \bfindex{formal @@ -330,7 +330,7 @@ *} -subsection {* Isabelle sessions *} +subsection {* Isabelle Sessions *} text {* In contrast to the highly interactive mode of the formal parts of @@ -377,7 +377,7 @@ with the generated document appearing in its proper place (within \verb,~/isabelle/browser_info,). - In practive, users may want to have \texttt{isatool mkdir} generate + In practice, users may want to have \texttt{isatool mkdir} generate an initial working setup without further ado. For example, an empty session \texttt{MySession} derived from \texttt{HOL} may be produced as follows: @@ -399,7 +399,10 @@ \texttt{MySession}, and the file \texttt{MySession/ROOT.ML} accordingly. \texttt{MySession/document/root.tex} should be also adapted at some point; the generated version is mostly - self-explanatory. + self-explanatory. The default versions includes the + \texttt{isabelle} (mandatory) and \texttt{isabellesym} (required for + mathematical symbols); further packages may required, e.g.\ for + unusual Isabelle symbols. Realistic applications may demand additional files in \texttt{MySession/document} for the {\LaTeX} stage, such as @@ -416,11 +419,13 @@ *} -subsection {* Structure markup *} +subsection {* Structure Markup *} subsubsection {* Sections *} text {* + FIXME \verb,\label, within sections; + The large-scale structure of Isabelle documents closely follows {\LaTeX} convention, with chapters, sections, subsubsections etc. The formal Isar language includes separate structure \bfindex{markup @@ -456,7 +461,8 @@ above. \medskip The following source fragment illustrates structure markup - of a theory. + of a theory. Note that {\LaTeX} labels may well be included inside + of section headings as well. \begin{ttbox} header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace} @@ -468,25 +474,26 @@ consts foo :: \dots bar :: \dots + defs \dots - + subsection {\ttlbrace}* Derived rules *{\ttrbrace} lemma fooI: \dots lemma fooE: \dots - subsection {\ttlbrace}* Main theorem *{\ttrbrace} + subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace} theorem main: \dots end \end{ttbox} - \medskip In realistic applications, users may well want to change - the meaning of some markup commands, typically via appropriate use - of \verb,\renewcommand, in \texttt{root.tex}. The - \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\ - moving it up in the hierarchy to become \verb,\chapter,. + Users may occasionally want to change the meaning of some markup + commands, typically via appropriate use of \verb,\renewcommand, in + \texttt{root.tex}. The \verb,\isamarkupheader, is a good candidate + for some adaption, e.g.\ moving it up in the hierarchy to become + \verb,\chapter,. \begin{verbatim} \renewcommand{\isamarkupheader}[1]{\chapter{#1}} @@ -495,12 +502,11 @@ Certainly, this requires to change the default \verb,\documentclass{article}, in \texttt{root.tex} to something that supports the notion of chapters in the first place, e.g.\ - \texttt{report} or \texttt{book}. + \verb,\documentclass{report},. - \medskip For each generated theory output the {\LaTeX} macro - \verb,\isabellecontext, holds the name of the formal context. This - is particularly useful for document headings or footings, e.g.\ like - this: + \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to + hold the name of the current theory context. This is particularly + useful for document headings or footings, e.g.\ like this: \begin{verbatim} \renewcommand{\isamarkupheader}[1]% @@ -508,33 +514,81 @@ \end{verbatim} \noindent Make sure to include something like - \verb,\pagestyle{headings}, in \texttt{root.tex} as well. Moreover, - the document should have more than 2 pages. + \verb,\pagestyle{headings}, in \texttt{root.tex}; the document + should have more than 2 pages to show the effect. *} -subsection {* Formal comments and antiquotations *} +subsection {* Formal Comments and Antiquotations *} text {* - Comments of the form \verb,(*,~\dots~\verb,*), + Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,), *} -subsection {* Symbols and characters *} +subsection {* Symbols and Characters *} text {* FIXME \verb,\isabellestyle, *} -subsection {* Suppressing output *} +subsection {* Suppressing Output *} text {* - FIXME \verb,no_document, + By default Isabelle's document system generates a {\LaTeX} source + file for each theory that happens to get loaded during the session. + The generated \texttt{session.tex} file will include all of these in + order of appearance, which in turn gets included by the standard + \texttt{root.tex} file. Certainly one may change the order of + appearance or suppress unwanted theories by ignoring + \texttt{session.tex} and include individual files in + \texttt{root.tex} by hand. On the other hand, such an arrangement + requires additional efforts for maintenance. + + Alternatively, one may tune the theory loading process in + \texttt{ROOT.ML}: traversal of the theory dependency graph may be + fine-tuned by adding further \verb,use_thy, invocations, although + topological sorting needs to be preserved. Moreover, the ML + operator \verb,no_document, temporarily disables document generation + while executing a theory loader command; the usage is like this: + +\begin{verbatim} + no_document use_thy "Aux"; +\end{verbatim} - FIXME \verb,(,\verb,*,\verb,<,\verb,*,\verb,), - \verb,(,\verb,*,\verb,>,\verb,*,\verb,), + Theory output may be also suppressed \emph{partially} as well. + Typical applications include research papers or slides based on + formal developments --- these usually do not show the full formal + content. The special source comments + \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and + \verb,(,\verb,*,\verb,>,\verb,*,\verb,), are interpreted by the + document generator as open and close parenthesis for + \bfindex{ignored material}. Any text inside of (potentially nested) + \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\dots~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), + parentheses is just ignored from the output --- after correct formal + checking. + + In the following example we suppress the slightly formalistic + \isakeyword{theory} and \isakeyword{end} part of a theory text. + + \medskip + + \begin{tabular}{l} + \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ + \texttt{theory A = Main:} \\ + \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ + ~~$\vdots$ \\ + \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ + \texttt{end} \\ + \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ + \end{tabular} + + \medskip + + Ignoring portions of printed text like this demands some special + care. FIXME *} (*<*)