# HG changeset patch # User wenzelm # Date 1010444234 -3600 # Node ID 2aa05eb15bd2df62ac1e58e5701185c17073a64c # Parent 3939e7dea202cfa064f8e02dcc3cb8f27ef93d70 getting close to completion; diff -r 3939e7dea202 -r 2aa05eb15bd2 doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Mon Jan 07 23:56:25 2002 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Mon Jan 07 23:57:14 2002 +0100 @@ -2,8 +2,6 @@ theory Documents = Main: (*>*) -(* FIXME exercises? *) - section {* Concrete Syntax \label{sec:concrete-syntax} *} text {* @@ -91,7 +89,7 @@ *} -subsection {* Mathematical Symbols *} +subsection {* Mathematical Symbols \label{sec:syntax-symbols} *} text {* Concrete syntax based on plain ASCII characters has its inherent @@ -418,7 +416,9 @@ \texttt{MySession}, and the file \texttt{MySession/ROOT.ML} accordingly. \texttt{MySession/document/root.tex} should be also adapted at some point; the default version is mostly - self-explanatory. + self-explanatory. Note that the \verb,\isabellestyle, enables + fine-tuning of the general appearance of characters and mathematical + symbols (see also \S\ref{sec:doc-prep-symbols}). Especially note the standard inclusion of {\LaTeX} packages \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required @@ -472,7 +472,7 @@ \medskip From the Isabelle perspective, each markup command takes a single - text argument (delimited by \verb,",\dots\verb,", or + $text$ argument (delimited by \verb,",\dots\verb,", or \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any surrounding white space, the argument is passed to a {\LaTeX} macro \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros @@ -540,17 +540,159 @@ subsection {* Formal Comments and Antiquotations *} text {* - Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,), + FIXME check + + Source comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,), + essentially act like white space and do not contribute to the formal + text at all. They mainly serve technical purposes to mark certain + oddities or problems with the raw sources. + + In contrast, \bfindex{formal comments} are portions of text that are + associated with formal Isabelle/Isar commands (\bfindex{marginal + comments}), or even as stanalone paragraphs positioned explicitly + within a theory or proof context (\bfindex{text blocks}). + + \medskip Marginal comments are part of each command's concrete + syntax \cite{isabelle-ref}; the common form \verb,--,~text, where + $text$, delimited by \verb,",\dots\verb,", or + \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as usual. Multiple marginal + comments may be given at the same time. Here is a simple example: + +\begin{verbatim} + lemma "A --> A" + -- "a triviality of propositional logic" + -- "(should not really bother)" + by (rule impI) -- "implicit assumption step involved here" +\end{verbatim} + + From the {\LaTeX} view, \verb,--, acts like a markup command, the + corresponding macro is \verb,\isamarkupcmt, (of a single argument). + + \medskip The commands \bfindex{text} and \bfindex{txt} both + introduce a text block (for theory and proof contexts, + respectively), taking a single $text$ argument. The {\LaTeX} output + appears as a free-form text, surrounded with separate paragraphs and + additional vertical spacing. This behavior is determined by the + {\LaTeX} environment definitions \verb,isamarkuptext, and + \verb,isamarkuptxt,, respectively. This may be changed via + \verb,\renewenvironment,, but it is often sufficient to redefine + \verb,\isastyletext, or \verb,\isastyletxt, only, which determine + the body text style. + + \medskip The $text$ part of each of the various markup commands + considered so far essentially inserts \emph{quoted} material within + a formal text, essentially for instruction of the reader only + (arbitrary {\LaTeX} macros may be included). + + An \bfindex{antiquotation} is again a formal object that has been + embedded into such an informal portion of text. Typically, the + interpretation of an antiquotation is limited to well-formedness + checks, with the result being pretty printed into the resulting + document output. So quoted text blocks together with antiquotations + provide very handsome means to reference formal entities within + informal expositions, with a high level of confidence in the + technical details (especially syntax and types). + + The general format of antiquotations is as follows: + \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or + \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}} + for a comma-separated list of $name$ or assignments + \texttt{$name$=$value$} of $options$ (see \cite{isabelle-isar-ref} + for details). The syntax of $arguments$ depends on the + antiquotation name, it generally follows the same conventions for + types, terms, or theorems as in the formal part of a theory. - FIXME + \medskip Here is an example use of the quotation-antiquotation + technique: @{term "%x y. x"} is a well-typed term. + + \medskip This output has been produced as follows: + \begin{ttbox} +text {\ttlbrace}* + Here is an example use of the quotation-antiquotation technique: + {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. +*{\ttrbrace} + \end{ttbox} + + From the notational change of the ASCII character \verb,%, to the + symbol @{text \} we see that the term really got printed by the + system --- recall that the document preparation system enables + symbolic output by default. + + \medskip In the following example we include an option to enable the + \verb,show_types, flag of Isabelle: the antiquotation + \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces @{term + [show_types] "%x y. x"}. Here type-inference has figured out the + most general typings in the present (theory) context. Within a + proof, one may get different results according to typings that have + already been figured out in the text so far, say some fixed + variables in the main statement given before hand. + + \medskip Several further kinds of antiquotations (and options) are + available \cite{isabelle-sys}. The most commonly used combinations + are as follows: + + \medskip + \begin{tabular}{ll} + \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ + \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ + \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ + \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ + \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ + \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ + \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\ + \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ + \end{tabular} + + \medskip + + Note that \verb,no_vars, given above is \emph{not} an option, but + merely an attribute of the theorem argument given here. + + The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is + particularly interesting. Embedding uninterpreted text within an + informal text body might appear useless at first sight. Here the + key virtue is that the string $s$ is processed as proper Isabelle + output, interpreting Isabelle symbols (\S\ref{sec:syntax-symbols}) + appropriately. + + For example, \texttt{\at}\verb,{text "\\"}, produces @{text "\\"}, + according to the standard interpretation of these symbol (cf.\ + \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent + mathematical notation in both the formal and informal parts of the + document very easily. Manual {\LaTeX} code leaves more control over + the type-setting, but is slightly more tedious. Also note that + Isabelle symbols may be also displayed within the editor buffer of + Proof~General. *} -subsection {* Symbols and Characters \label{sec:doc-prep-symbols} *} +subsection {* Interpretation of symbols \label{sec:doc-prep-symbols} *} text {* - FIXME \verb,\isabellestyle, + FIXME tune + + According to \S\ref{sec:syntax-symbols}, the smalles syntactic + entities of Isabelle text are symbols, a straight-forward + generalization of ASCII characters. Concerning document + preperation, symbols are translated uniformly to {\LaTeX} code as + follows. + + \begin{enumerate} \item 7-bit ASCII characters: letters + \texttt{A\dots Z} and \texttt{a\dots z} are output verbatim, digits + are passed as an argument to the \verb,\isadigit, macro, other + characters are replaced by specific macros \verb,\isacharXYZ, (see + also \texttt{isabelle.sty}). + + \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become + \verb,\{\isasym,$XYZ$\verb,}, each (note the additional braces). + See \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for + the collection of predefined standard symbols. + + \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, become + \verb,\isactrl,$XYZ$; subsequent symbols may act as arguments, if + the corresponding macro is defined accordingly. + \end{enumerate} *} @@ -619,7 +761,8 @@ \begin{verbatim} by (auto(*<*)simp add: int_less_le(*>*)) -\end{verbatim} %(* +\end{verbatim} +%(* \medskip Ignoring portions of printed does demand some care by the user. First of all, the writer is responsible not to obfuscate the