
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 \<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
@@ -264,7 +264,7 @@
   currency :: "currency \<Rightarrow> nat"    ("\<currency>")
 
 
-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"\<noteq>"}, 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
 *}
 
 (*<*)




