--- a/doc-src/TutorialI/Documents/document/Documents.tex Sun Jan 06 13:47:26 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Sun Jan 06 13:47:55 2002 +0100
@@ -3,7 +3,7 @@
\def\isabellecontext{Documents}%
\isamarkupfalse%
%
-\isamarkupsection{Concrete syntax \label{sec:concrete-syntax}%
+\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
}
\isamarkuptrue%
%
@@ -27,7 +27,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Infix annotations%
+\isamarkupsubsection{Infix Annotations%
}
\isamarkuptrue%
%
@@ -85,7 +85,7 @@
\isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. 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
@@ -108,7 +108,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Mathematical symbols \label{sec:thy-present-symbols}%
+\isamarkupsubsection{Mathematical Symbols \label{sec:thy-present-symbols}%
}
\isamarkuptrue%
%
@@ -218,7 +218,7 @@
\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
%
-\isamarkupsubsection{Prefix annotations%
+\isamarkupsubsection{Prefix Annotations%
}
\isamarkuptrue%
%
@@ -261,7 +261,7 @@
\isacommand{consts}\isanewline
\ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
%
-\isamarkupsubsection{Syntax translations \label{sec:def-translations}%
+\isamarkupsubsection{Syntax Translations \label{sec:def-translations}%
}
\isamarkuptrue%
%
@@ -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 \isa{{\isasymnoteq}}, since existing theorems
about \isa{{\isacharequal}} still apply.%
@@ -300,7 +300,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Document preparation%
+\isamarkupsection{Document Preparation%
}
\isamarkuptrue%
%
@@ -332,7 +332,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Isabelle sessions%
+\isamarkupsubsection{Isabelle Sessions%
}
\isamarkuptrue%
%
@@ -381,7 +381,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:
@@ -403,7 +403,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
@@ -420,7 +423,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Structure markup%
+\isamarkupsubsection{Structure Markup%
}
\isamarkuptrue%
%
@@ -429,7 +432,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The large-scale structure of Isabelle documents closely follows
+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
commands}, which do not effect the formal content of a theory (or
@@ -464,7 +469,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}
@@ -476,25 +482,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}}
@@ -503,12 +510,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]%
@@ -516,21 +522,21 @@
\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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Formal comments and antiquotations%
+\isamarkupsubsection{Formal Comments and Antiquotations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Comments of the form \verb,(*,~\dots~\verb,*),%
+Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Symbols and characters%
+\isamarkupsubsection{Symbols and Characters%
}
\isamarkuptrue%
%
@@ -539,15 +545,63 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Suppressing output%
+\isamarkupsubsection{Suppressing Output%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%