doc-src/TutorialI/Documents/Documents.thy

 (*<*)
 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
   \<lambda>}-calculus, the core concept of Isabelle's elaborate infrastructure
   for concrete syntax is that of general \bfindex{mixfix annotations}.

   \medskip Subsequently we introduce a few simple declaration forms
   that already cover the most common situations fairly well.
 *}
 
 
-subsection {* Infix annotations *}
+subsection {* Infix Annotations *}
 
 text {*
   Syntax annotations may be included wherever constants are declared
   directly or indirectly, including \isacommand{consts},
   \isacommand{constdefs}, or \isacommand{datatype} (for the

   [+] C"} stands for @{text "(A [+] B) [+] C"}.  Similarly,
   \isakeyword{infixr} refers to nesting to the \emph{right}, reading
   @{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
   explicitly within the logic.  Exclusive-or is happens to be
   associative, as shown below.

   one may consider to force parentheses by use of non-oriented infix
   syntax; equality would probably be a typical candidate.
 *}
 
 
-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
   limitations.  Rich mathematical notation demands a larger repertoire
   of symbols.  Several standards of extended character sets have been

 
 syntax (xsymbols output)
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>\<ignore>" 60)
 
 
-subsection {* Prefix annotations *}
+subsection {* Prefix Annotations *}
 
 text {*
   Prefix syntax annotations\index{prefix annotation} are just a very
   degenerate of the general mixfix form \cite{isabelle-ref}, without
   any template arguments or priorities --- just some piece of literal

 
 consts
   currency :: "currency \<Rightarrow> nat"    ("\<currency>")
 
 
-subsection {* Syntax translations \label{sec:def-translations} *}
+subsection {* Syntax Translations \label{sec:def-translations} *}
 
 text{*
   FIXME
 
 \index{syntax translations|(}%

 and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
 for uni-directional translations, which only affect
 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"\<noteq>"}, since existing theorems
 about @{text"="} still apply.%
 \index{syntax translations|)}%
 \index{translations@\isacommand {translations} (command)|)}
 *}
 
 
-section {* Document preparation *}
+section {* Document Preparation *}
 
 text {*
   Isabelle/Isar is centered around a certain notion of \bfindex{formal
   proof documents}\index{documents|bold}: ultimately the result of the
   user's theory development efforts is a human-readable record --- as

   reports on formal theory developments with little additional effort,
   the most tedious consistency checks are handled by the system.
 *}
 
 
-subsection {* Isabelle sessions *}
+subsection {* Isabelle Sessions *}
 
 text {*
   In contrast to the highly interactive mode of the formal parts of
   Isabelle/Isar theory development, the document preparation stage
   essentially works in batch-mode.  This revolves around the concept

   With everything put in its proper place, \texttt{isatool make}
   should be sufficient to process the Isabelle session completely,
   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:
 
 \begin{verbatim}

 
   \medskip Users may now start to populate the directory
   \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
   \texttt{root.bib} for the bibliographic database.\footnote{Using
   that particular name of \texttt{root.bib}, the Isabelle document

   {\LaTeX} errors, users may trace error messages at the file position
   of the generated text.
 *}
 
 
-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
   commands}, which do not effect the formal content of a theory (or
   proof), but results in corresponding {\LaTeX} elements issued to the

   \verb,\isamarkupXXX, for any command \isakeyword{XXX}.  The latter
   are defined in \verb,isabelle.sty, according to the rightmost column
   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}
 
   theory Foo_Bar = Main:

   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
 
   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}}
 \end{verbatim}
 
   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}.
-
-  \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:
+  \verb,\documentclass{report},.
+
+  \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]%
   {\chapter{#1}\markright{THEORY~\isabellecontext}}
 \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.
-*}
-
-
-subsection {* Formal comments and antiquotations *}
-
-text {*
-  Comments of the form \verb,(*,~\dots~\verb,*),
-
-*}
-
-
-subsection {* Symbols and characters *}
+  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
+  should have more than 2 pages to show the effect.
+*}
+
+
+subsection {* Formal Comments and Antiquotations *}
+
+text {*
+  Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
+
+*}
+
+
+subsection {* Symbols and Characters *}
 
 text {*
   FIXME \verb,\isabellestyle,
 *}
 
 
-subsection {* Suppressing output *}
-
-text {*
-  FIXME \verb,no_document,
-
-  FIXME \verb,(,\verb,*,\verb,<,\verb,*,\verb,),
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,),
+subsection {* Suppressing Output *}
+
+text {*
+  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}
+
+  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
 (*>*)