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>\, 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++), \isa{{\isasymbeta}}, etc apart from - \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}} - (\verb+\+\verb++) and \isa{{\isasymAA}} (\verb+\+\verb++), - 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++), \isa{{\isasymbeta}} + (\verb+\+\verb++), etc. (excluding \isa{{\isasymlambda}}), + special letters like \isa{{\isasymA}} (\verb+\+\verb++) and \isa{{\isasymAA}} (\verb+\+\verb++), 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,\,\verb,\<^isub>1.\,\verb,\<^isub>1=\,\verb,\<^isup>\,} + {\small\noindent \verb,\,\verb,\,\verb,\<^isub>1.,~\verb,\,\verb,\<^isub>1 = \,\verb,\<^isup>\,} \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% %