# HG changeset patch # User wenzelm # Date 1226608356 -3600 # Node ID 99f6da3bbbf73cb5ed3e5a76f65f0ccd722ef988 # Parent 69268a097405374529caa02f46d71bbe9393da9c renamed "formal comments" to "document comments"; tuned section "Markup commands"; updated/tuned section "Document Antiquotations"; diff -r 69268a097405 -r 99f6da3bbbf7 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:31:25 2008 +0100 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:32:36 2008 +0100 @@ -101,11 +101,13 @@ subsection}, and @{command subsubsection}] mark chapter and section headings within the main theory body or local theory targets. The corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"}, - @{verbatim "\\isamarkupsection"} etc. + @{verbatim "\\isamarkupsection"}, @{verbatim + "\\isamarkupsubsection"} etc. \item [@{command sect}, @{command subsect}, and @{command subsubsect}] mark section headings within proofs. The corresponding - {\LaTeX} macros are @{verbatim "\\isamarkupsect"} etc. + {\LaTeX} macros are @{verbatim "\\isamarkupsect"}, @{verbatim + "\\isamarkupsubsect"} etc. \item [@{command text} and @{command txt}] specify paragraphs of plain text. This corresponds to a {\LaTeX} environment @{verbatim @@ -121,19 +123,18 @@ Except for @{command "text_raw"} and @{command "txt_raw"}, the text passed to any of the above markup commands may refer to formal - entities via \emph{antiquotations}, see also \secref{sec:antiq}. - These are interpreted in the present theory or proof context, or the - named @{text "target"}. + entities via \emph{document antiquotations}, see also + \secref{sec:antiq}. These are interpreted in the present theory or + proof context, or the named @{text "target"}. \medskip The proof markup commands closely resemble those for theory specifications, but have a different formal status and produce - different {\LaTeX} macros (although the default definitions coincide - for analogous commands such as @{command section} and @{command - sect}). + different {\LaTeX} macros. The default definitions coincide for + analogous commands such as @{command section} and @{command sect}. *} -section {* Antiquotations \label{sec:antiq} *} +section {* Document Antiquotations \label{sec:antiq} *} text {* \begin{matharray}{rcl} @@ -158,18 +159,24 @@ @{antiquotation_def ML_struct} & : & \isarantiq \\ \end{matharray} - The text body of formal comments (see also \secref{sec:comments}) - may contain antiquotations of logical entities, such as theorems, - terms and types, which are to be presented in the final output - produced by the Isabelle document preparation system. + The overall content of an Isabelle/Isar theory may alternate between + formal and informal text. The main body consists of formal + specification and proof commands, interspersed with markup commands + (\secref{sec:markup}) or document comments (\secref{sec:comments}). + The argument of markup commands quotes informal text to be printed + in the resulting document, but may again refer to formal entities + via \emph{document antiquotations}. - Thus embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}'' - within a text block would cause - \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document. Also note that theorem - antiquotations may involve attributes as well. For example, - @{text "@{thm sym [no_vars]}"} would print the theorem's - statement where all schematic variables have been replaced by fixed - ones, which are easier to read. + For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}'' + within a text block makes + \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document. + + Antiquotations usually spare the author tedious typing of logical + entities in full detail. Even more importantly, some degree of + consistency-checking between the main body of formal text and its + informal explanation is achieved, since terms and types appearing in + antiquotations are checked within the current theory or proof + context. \begin{rail} atsign lbrace antiquotation rbrace @@ -203,7 +210,7 @@ \end{rail} Note that the syntax of antiquotations may \emph{not} include source - comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} or verbatim + comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} nor verbatim text @{verbatim "{"}@{verbatim "*"}~@{text "\"}~@{verbatim "*"}@{verbatim "}"}. @@ -213,17 +220,15 @@ guaranteed to refer to a valid ancestor theory in the current context. - \item [@{text "@{thm a\<^sub>1 \ a\<^sub>n}"}] prints theorems - @{text "a\<^sub>1 \ a\<^sub>n"}. Note that attribute specifications - may be included as well (see also \secref{sec:syn-att}); the - @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would - be particularly useful to suppress printing of schematic variables. + \item [@{text "@{thm a\<^sub>1 \ a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. + Full fact expressions are allowed here, including attributes + (\secref{sec:syn-att}). \item [@{text "@{prop \}"}] prints a well-typed proposition @{text "\"}. - \item [@{text "@{lemma \ by m}"}] asserts a well-typed proposition @{text - "\"} to be provable by method @{text m} and prints @{text "\"}. + \item [@{text "@{lemma \ by m}"}] proves a well-typed proposition + @{text "\"} by method @{text m} and prints the original @{text "\"}. \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}. @@ -247,45 +252,50 @@ \item [@{text "@{text s}"}] prints uninterpreted source text @{text s}. This is particularly useful to print portions of text according - to the Isabelle {\LaTeX} output style, without demanding - well-formedness (e.g.\ small pieces of terms that should not be - parsed or type-checked yet). + to the Isabelle document style, without demanding well-formedness, + e.g.\ small pieces of terms that should not be parsed or + type-checked yet. \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal state. This is mainly for support of tactic-emulation scripts - within Isar --- presentation of goal states does not conform to - actual human-readable proof documents. + within Isar. Presentation of goal states does not conform to the + idea of human-readable proof documents! - Please do not include goal states into document output unless you - really know what you are doing! + When explaining proofs in detail it is usually better to spell out + the reasoning via proper Isar proof commands, instead of peeking at + the internal machine configuration. \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but does not print the main goal. - \item [@{text "@{prf a\<^sub>1 \ a\<^sub>n}"}] prints the (compact) - proof terms corresponding to the theorems @{text "a\<^sub>1 \ - a\<^sub>n"}. Note that this requires proof terms to be switched on - for the current object logic (see the ``Proof terms'' section of the - Isabelle reference manual for information on how to do this). + \item [@{text "@{prf a\<^sub>1 \ a\<^sub>n}"}] prints the (compact) proof terms + corresponding to the theorems @{text "a\<^sub>1 \ a\<^sub>n"}. Note that this + requires proof terms to be switched on for the current logic + session. \item [@{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"}] is like @{text - "@{prf a\<^sub>1 \ a\<^sub>n}"}, but displays the full proof terms, - i.e.\ also displays information omitted in the compact proof term, - which is denoted by ``@{text _}'' placeholders there. + "@{prf a\<^sub>1 \ a\<^sub>n}"}, but prints the full proof terms, i.e.\ also + displays information omitted in the compact proof term, which is + denoted by ``@{text _}'' placeholders there. \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text "@{ML_struct s}"}] check text @{text s} as ML value, type, and - structure, respectively. The source is displayed verbatim. + structure, respectively. The source is printed verbatim. \end{descr} +*} - \medskip The following standard styles for use with @{text - thm_style} and @{text term_style} are available: + +subsubsection {* Styled antiquotations *} + +text {* Some antiquotations like @{text thm_style} and @{text + term_style} admit an extra \emph{style} specification to modify the + printed result. The following standard styles are available: \begin{descr} \item [@{text lhs}] extracts the first argument of any application - form with at least two arguments -- typically meta-level or + form with at least two arguments --- typically meta-level or object-level equality, or any other binary relation. \item [@{text rhs}] is like @{text lhs}, but extracts the second @@ -299,10 +309,14 @@ Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} \end{descr} +*} - \medskip - The following options are available to tune the output. Note that most of - these coincide with ML flags of the same names (see also \cite{isabelle-ref}). + +subsubsection {* General options *} + +text {* The following options are available to tune the printed output + of antiquotations. Note that many of these coincide with global ML + flags of the same names. \begin{descr} @@ -333,6 +347,9 @@ output as multi-line ``display material'', rather than a small piece of text without line breaks (which is the default). + In this mode the embedded entities are printed in the same style as + the main theory text. + \item[@{text "break = bool"}] controls line breaks in non-display material. @@ -347,29 +364,35 @@ \item[@{text "margin = nat"} and @{text "indent = nat"}] change the margin or indentation for pretty printing of display material. - \item[@{text "source = bool"}] prints the source text of the - antiquotation arguments, rather than the actual value. Note that - this does not affect well-formedness checks of @{antiquotation - "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation - "text"} antiquotation admits arbitrary output). - \item[@{text "goals_limit = nat"}] determines the maximum number of - goals to be printed. + goals to be printed (for goal-based antiquotation). \item[@{text "locale = name"}] specifies an alternative locale context used for evaluating and printing the subsequent argument. + \item[@{text "source = bool"}] prints the original source text of + the antiquotation arguments, rather than its internal + representation. Note that formal checking of @{antiquotation + "thm"}, @{antiquotation "term"}, etc. is still enabled; use the + @{antiquotation "text"} antiquotation for unchecked output. + + Regular @{text "term"} and @{text "typ"} antiquotations with @{text + "source = false"} involve a full round-trip from the original source + to an internalized logical entity back to a source form, according + to the syntax of the current context. Thus the printed output is + not under direct control of the author, it may even fluctuate a bit + as the underlying theory is changed later on. + + In contrast, @{text "source = true"} admits direct printing of the + given source text, with the desirable well-formedness check in the + background, but without modification of the printed text. + \end{descr} For boolean flags, ``@{text "name = true"}'' may be abbreviated as ``@{text name}''. All of the above flags are disabled by default, - unless changed from ML. - - \medskip Note that antiquotations do not only spare the author from - tedious typing of logical entities, but also achieve some degree of - consistency-checking of informal explanations with formal - developments: well-formedness of terms and types with respect to the - current theory or proof context is ensured here. + unless changed from ML, say in the @{verbatim "ROOT.ML"} of the + logic session. *}