
diff -r 797433ca1ab3 -r 45bee2f6e61f doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Documents}%
-\isamarkupfalse%
 %
 \isadelimtheory
 %
@@ -134,26 +133,24 @@
   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
   output as \isa{A\isactrlsup {\isasymstar}}.
 
-  A number of symbols are considered letters by the Isabelle lexer 
-  and can be used as part of identifiers. These are the greek letters
-  \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}, etc apart from
-  \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}}
-  (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+), 
-  and the special control symbols \verb+\+\verb+<^isub>+ and 
-  \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
-  means that the input 
+  A number of symbols are considered letters by the Isabelle lexer and
+  can be used as part of identifiers. These are the greek letters
+  \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}
+  (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isasymlambda}}),
+  special letters like \isa{{\isasymA}} (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+), and the control symbols
+  \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
+  sub and super scripts. This means that the input
 
   \medskip
-  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
+  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
 
   \medskip
   \noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}} 
-  by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single entity like 
-  \isa{PA}, not an exponentiation.
+  by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single
+  syntactic entity, not an exponentiation.
 
-
-  \medskip Replacing our definition of \isa{xor} by the following
-  specifies an Isabelle symbol for the new operator:%
+  \medskip Replacing our previous definition of \isa{xor} by the
+  following specifies an Isabelle symbol for the new operator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -425,10 +422,7 @@
   location of the ultimate results.  The above dry run should be able
   to produce some \texttt{document.pdf} (with dummy title, empty table
   of contents etc.).  Any failure at this stage usually indicates
-  technical problems of the {\LaTeX} installation.\footnote{Especially
-  make sure that \texttt{pdflatex} is present; if in doubt one may
-  fall back on DVI output by changing \texttt{usedir} options in
-  \texttt{IsaMakefile} \cite{isabelle-sys}.}
+  technical problems of the {\LaTeX} installation.
 
   \medskip The detailed arrangement of the session sources is as
   follows.
@@ -826,37 +820,54 @@
   no_document use_thy "T";
 \end{verbatim}
 
-  \medskip Theory output may be suppressed more selectively.  Research
-  articles and slides usually do not include the formal content in
-  full.  Delimiting \bfindex{ignored material} by the special source
-  comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
-  preparation system to suppress these parts; the formal checking of
-  the theory is unchanged, of course.
-
-  In this example, we hide a theory's \isakeyword{theory} and
-  \isakeyword{end} brackets:
-
-  \medskip
+  \medskip Theory output may be suppressed more selectively, either
+  via \bfindex{tagged command regions} or \bfindex{ignored material}.
 
-  \begin{tabular}{l}
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{theory T} \\
-  \texttt{imports Main} \\
-  \texttt{begin} \\
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
-  ~~$\vdots$ \\
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{end} \\
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
-  \end{tabular}
+  Tagged command regions works by annotating commands with named tags,
+  which correspond to certain {\LaTeX} markup that tells how to treat
+  particular parts of a document when doing the actual type-setting.
+  By default, certain Isabelle/Isar commands are implicitly marked up
+  using the predefined tags ``\emph{theory}'' (for theory begin and
+  end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
+  commands involving ML code).  Users may add their own tags using the
+  \verb,%,\emph{tag} notation right after a command name.  In the
+  subsequent example we hide a particularly irrelevant proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\isadeliminvisible
+\ %
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharparenright}%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\begin{isamarkuptext}%
+The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
+  Tags observe the structure of proofs; adjacent commands with the
+  same tag are joined into a single region.  The Isabelle document
+  preparation system allows the user to specify how to interpret a
+  tagged region, in order to keep, drop, or fold the corresponding
+  parts of the document.  See the \emph{Isabelle System Manual}
+  \cite{isabelle-sys} for further details, especially on
+  \texttt{isatool usedir} and \texttt{isatool document}.
 
-  \medskip
-
-  Text may be suppressed in a fine-grained manner.  We may even hide
-  vital parts of a proof, pretending that things have been simpler
-  than they really were.  For example, this ``fully automatic'' proof
-  is actually a fake:%
+  Ignored material is specified by delimiting the original formal
+  source with special source comments
+  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+  \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
+  before the type-setting phase, without affecting the formal checking
+  of the theory, of course.  For example, we may hide parts of a proof
+  that seem unfit for general public inspection.  The following
+  ``fully automatic'' proof is actually a fake:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
@@ -877,7 +888,7 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-\noindent Here the real source of the proof has been as follows:
+\noindent The real source of the proof has been as follows:
 
 \begin{verbatim}
   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
@@ -887,23 +898,7 @@
   \medskip Suppressing portions of printed text demands care.  You
   should not misrepresent the underlying theory development.  It is
   easy to invalidate the visible text by hiding references to
-  questionable axioms.
-
-% I removed this because the page overflowed and I disagree a little. TN
-%
-%  Authentic reports of Isabelle/Isar theories, say as part of a
-% library, should suppress nothing.  Other users may need the full
-% information for their own derivative work.  If a particular
-% formalization appears inadequate for general public coverage, it is
-% often more appropriate to think of a better way in the first place.
-
-  \medskip Some technical subtleties of the
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
-  elements need to be kept in mind, too --- the system performs few
-  sanity checks here.  Arguments of markup commands and formal
-  comments must not be hidden, otherwise presentation fails.  Open and
-  close parentheses need to be inserted carefully; it is easy to hide
-  the wrong parts, especially after rearranging the theory text.%
+  questionable axioms.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %




