wenzelm@27043: theory Document_Preparation wenzelm@42651: imports Base Main wenzelm@27043: begin wenzelm@27043: wenzelm@27043: chapter {* Document preparation \label{ch:document-prep} *} wenzelm@27043: wenzelm@28746: text {* Isabelle/Isar provides a simple document preparation system wenzelm@54346: based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks wenzelm@54346: within that format. This allows to produce papers, books, theses wenzelm@54346: etc.\ from Isabelle theory sources. wenzelm@27043: wenzelm@51057: {\LaTeX} output is generated while processing a \emph{session} in wenzelm@51057: batch mode, as explained in the \emph{The Isabelle System Manual} wenzelm@51057: \cite{isabelle-sys}. The main Isabelle tools to get started with wenzelm@54346: document preparation are @{tool_ref mkroot} and @{tool_ref build}. wenzelm@27043: wenzelm@54346: The classic Isabelle/HOL tutorial \cite{isabelle-hol-book} also wenzelm@54346: explains some aspects of theory presentation. *} wenzelm@27043: wenzelm@27043: wenzelm@27043: section {* Markup commands \label{sec:markup} *} wenzelm@27043: wenzelm@27043: text {* wenzelm@27043: \begin{matharray}{rcl} wenzelm@28761: @{command_def "header"} & : & @{text "toplevel \ toplevel"} \\[0.5ex] wenzelm@28761: @{command_def "chapter"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def "section"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def "subsection"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def "subsubsection"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def "text"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def "text_raw"} & : & @{text "local_theory \ local_theory"} \\[0.5ex] wenzelm@28761: @{command_def "sect"} & : & @{text "proof \ proof"} \\ wenzelm@28761: @{command_def "subsect"} & : & @{text "proof \ proof"} \\ wenzelm@28761: @{command_def "subsubsect"} & : & @{text "proof \ proof"} \\ wenzelm@28761: @{command_def "txt"} & : & @{text "proof \ proof"} \\ wenzelm@28761: @{command_def "txt_raw"} & : & @{text "proof \ proof"} \\ wenzelm@27043: \end{matharray} wenzelm@27043: wenzelm@28747: Markup commands provide a structured way to insert text into the wenzelm@28747: document generated from a theory. Each markup command takes a wenzelm@28747: single @{syntax text} argument, which is passed as argument to a wenzelm@28747: corresponding {\LaTeX} macro. The default macros provided by wenzelm@40800: @{file "~~/lib/texinputs/isabelle.sty"} can be redefined according wenzelm@28747: to the needs of the underlying document and {\LaTeX} styles. wenzelm@28747: wenzelm@28747: Note that formal comments (\secref{sec:comments}) are similar to wenzelm@28747: markup commands, but have a different status within Isabelle/Isar wenzelm@28747: syntax. wenzelm@27043: wenzelm@42596: @{rail " wenzelm@42596: (@@{command chapter} | @@{command section} | @@{command subsection} | wenzelm@42596: @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text} wenzelm@27043: ; wenzelm@42596: (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} | wenzelm@42596: @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text} wenzelm@42596: "} wenzelm@27043: wenzelm@28760: \begin{description} wenzelm@27043: wenzelm@28760: \item @{command header} provides plain text markup just preceding wenzelm@28747: the formal beginning of a theory. The corresponding {\LaTeX} macro wenzelm@28747: is @{verbatim "\\isamarkupheader"}, which acts like @{command wenzelm@28747: section} by default. wenzelm@27049: wenzelm@28760: \item @{command chapter}, @{command section}, @{command subsection}, wenzelm@28760: and @{command subsubsection} mark chapter and section headings wenzelm@28760: within the main theory body or local theory targets. The wenzelm@28747: corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"}, wenzelm@28749: @{verbatim "\\isamarkupsection"}, @{verbatim wenzelm@28749: "\\isamarkupsubsection"} etc. wenzelm@28747: wenzelm@28760: \item @{command sect}, @{command subsect}, and @{command subsubsect} wenzelm@28760: mark section headings within proofs. The corresponding {\LaTeX} wenzelm@28760: macros are @{verbatim "\\isamarkupsect"}, @{verbatim wenzelm@28749: "\\isamarkupsubsect"} etc. wenzelm@27043: wenzelm@28760: \item @{command text} and @{command txt} specify paragraphs of plain wenzelm@28760: text. This corresponds to a {\LaTeX} environment @{verbatim wenzelm@28747: "\\begin{isamarkuptext}"} @{text "\"} @{verbatim wenzelm@28747: "\\end{isamarkuptext}"} etc. wenzelm@27043: wenzelm@28760: \item @{command text_raw} and @{command txt_raw} insert {\LaTeX} wenzelm@28747: source into the output, without additional markup. Thus the full wenzelm@28747: range of document manipulations becomes available, at the risk of wenzelm@28747: messing up document output. wenzelm@27043: wenzelm@28760: \end{description} wenzelm@27043: wenzelm@28747: Except for @{command "text_raw"} and @{command "txt_raw"}, the text wenzelm@28747: passed to any of the above markup commands may refer to formal wenzelm@28749: entities via \emph{document antiquotations}, see also wenzelm@28749: \secref{sec:antiq}. These are interpreted in the present theory or wenzelm@28749: proof context, or the named @{text "target"}. wenzelm@27043: wenzelm@27043: \medskip The proof markup commands closely resemble those for theory wenzelm@27043: specifications, but have a different formal status and produce wenzelm@28749: different {\LaTeX} macros. The default definitions coincide for wenzelm@28749: analogous commands such as @{command section} and @{command sect}. wenzelm@27043: *} wenzelm@27043: wenzelm@27043: wenzelm@28749: section {* Document Antiquotations \label{sec:antiq} *} wenzelm@27043: wenzelm@27043: text {* wenzelm@27043: \begin{matharray}{rcl} wenzelm@28761: @{antiquotation_def "theory"} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def "thm"} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def "lemma"} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def "prop"} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def "term"} & : & @{text antiquotation} \\ haftmann@32898: @{antiquotation_def term_type} & : & @{text antiquotation} \\ haftmann@32898: @{antiquotation_def typeof} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def const} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def abbrev} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def typ} & : & @{text antiquotation} \\ haftmann@39305: @{antiquotation_def type} & : & @{text antiquotation} \\ haftmann@39305: @{antiquotation_def class} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def "text"} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def goals} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def subgoals} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def prf} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def full_prf} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def ML} & : & @{text antiquotation} \\ wenzelm@46261: @{antiquotation_def ML_op} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def ML_type} & : & @{text antiquotation} \\ wenzelm@28761: @{antiquotation_def ML_struct} & : & @{text antiquotation} \\ wenzelm@40801: @{antiquotation_def "file"} & : & @{text antiquotation} \\ wenzelm@54702: @{antiquotation_def "url"} & : & @{text antiquotation} \\ wenzelm@27043: \end{matharray} wenzelm@27043: wenzelm@28749: The overall content of an Isabelle/Isar theory may alternate between wenzelm@28749: formal and informal text. The main body consists of formal wenzelm@28749: specification and proof commands, interspersed with markup commands wenzelm@28749: (\secref{sec:markup}) or document comments (\secref{sec:comments}). wenzelm@28749: The argument of markup commands quotes informal text to be printed wenzelm@28749: in the resulting document, but may again refer to formal entities wenzelm@28749: via \emph{document antiquotations}. wenzelm@27043: wenzelm@28749: For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}'' wenzelm@28749: within a text block makes wenzelm@28749: \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. wenzelm@28749: wenzelm@28749: Antiquotations usually spare the author tedious typing of logical wenzelm@28749: entities in full detail. Even more importantly, some degree of wenzelm@28749: consistency-checking between the main body of formal text and its wenzelm@28749: informal explanation is achieved, since terms and types appearing in wenzelm@28749: antiquotations are checked within the current theory or proof wenzelm@28749: context. wenzelm@27043: wenzelm@43618: %% FIXME less monolithic presentation, move to individual sections!? wenzelm@42596: @{rail " wenzelm@42596: '@{' antiquotation '}' wenzelm@27043: ; wenzelm@42596: @{syntax_def antiquotation}: wenzelm@42596: @@{antiquotation theory} options @{syntax name} | wenzelm@42596: @@{antiquotation thm} options styles @{syntax thmrefs} | wenzelm@42617: @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? | wenzelm@42596: @@{antiquotation prop} options styles @{syntax prop} | wenzelm@42596: @@{antiquotation term} options styles @{syntax term} | wenzelm@43618: @@{antiquotation (HOL) value} options styles @{syntax term} | wenzelm@42596: @@{antiquotation term_type} options styles @{syntax term} | wenzelm@42596: @@{antiquotation typeof} options styles @{syntax term} | wenzelm@42596: @@{antiquotation const} options @{syntax term} | wenzelm@42596: @@{antiquotation abbrev} options @{syntax term} | wenzelm@42596: @@{antiquotation typ} options @{syntax type} | wenzelm@42596: @@{antiquotation type} options @{syntax name} | wenzelm@42596: @@{antiquotation class} options @{syntax name} | wenzelm@46261: @@{antiquotation text} options @{syntax name} wenzelm@46261: ; wenzelm@46261: @{syntax antiquotation}: wenzelm@42596: @@{antiquotation goals} options | wenzelm@42596: @@{antiquotation subgoals} options | wenzelm@42596: @@{antiquotation prf} options @{syntax thmrefs} | wenzelm@42596: @@{antiquotation full_prf} options @{syntax thmrefs} | wenzelm@42596: @@{antiquotation ML} options @{syntax name} | wenzelm@46261: @@{antiquotation ML_op} options @{syntax name} | wenzelm@42596: @@{antiquotation ML_type} options @{syntax name} | wenzelm@42596: @@{antiquotation ML_struct} options @{syntax name} | wenzelm@54702: @@{antiquotation \"file\"} options @{syntax name} | wenzelm@54705: @@{antiquotation file_unchecked} options @{syntax name} | wenzelm@54702: @@{antiquotation url} options @{syntax name} wenzelm@27043: ; wenzelm@27043: options: '[' (option * ',') ']' wenzelm@27043: ; wenzelm@42596: option: @{syntax name} | @{syntax name} '=' @{syntax name} wenzelm@27043: ; haftmann@32892: styles: '(' (style + ',') ')' haftmann@32891: ; wenzelm@42596: style: (@{syntax name} +) wenzelm@42617: "} wenzelm@27043: wenzelm@27043: Note that the syntax of antiquotations may \emph{not} include source wenzelm@28749: comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} nor verbatim wenzelm@27043: text @{verbatim "{"}@{verbatim "*"}~@{text "\"}~@{verbatim wenzelm@27043: "*"}@{verbatim "}"}. wenzelm@27043: wenzelm@28760: \begin{description} wenzelm@27043: wenzelm@28760: \item @{text "@{theory A}"} prints the name @{text "A"}, which is wenzelm@27043: guaranteed to refer to a valid ancestor theory in the current wenzelm@27043: context. wenzelm@27043: wenzelm@28760: \item @{text "@{thm a\<^sub>1 \ a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. wenzelm@28749: Full fact expressions are allowed here, including attributes wenzelm@28749: (\secref{sec:syn-att}). wenzelm@27043: wenzelm@28760: \item @{text "@{prop \}"} prints a well-typed proposition @{text wenzelm@27043: "\"}. wenzelm@27043: wenzelm@28760: \item @{text "@{lemma \ by m}"} proves a well-typed proposition wenzelm@28749: @{text "\"} by method @{text m} and prints the original @{text "\"}. haftmann@27453: wenzelm@28760: \item @{text "@{term t}"} prints a well-typed term @{text "t"}. bulwahn@43613: wenzelm@43618: \item @{text "@{value t}"} evaluates a term @{text "t"} and prints wenzelm@43618: its result, see also @{command_ref (HOL) value}. wenzelm@27043: haftmann@32898: \item @{text "@{term_type t}"} prints a well-typed term @{text "t"} haftmann@32898: annotated with its type. haftmann@32898: haftmann@32898: \item @{text "@{typeof t}"} prints the type of a well-typed term haftmann@32898: @{text "t"}. haftmann@32898: wenzelm@28760: \item @{text "@{const c}"} prints a logical or syntactic constant wenzelm@27043: @{text "c"}. wenzelm@27043: wenzelm@28760: \item @{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"} prints a constant abbreviation wenzelm@28760: @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in the current context. haftmann@39305: wenzelm@28760: \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. haftmann@39305: wenzelm@39689: \item @{text "@{type \}"} prints a (logical or syntactic) type wenzelm@39689: constructor @{text "\"}. haftmann@39305: haftmann@39305: \item @{text "@{class c}"} prints a class @{text c}. haftmann@39305: wenzelm@28760: \item @{text "@{text s}"} prints uninterpreted source text @{text wenzelm@27043: s}. This is particularly useful to print portions of text according wenzelm@28749: to the Isabelle document style, without demanding well-formedness, wenzelm@28749: e.g.\ small pieces of terms that should not be parsed or wenzelm@28749: type-checked yet. wenzelm@27043: wenzelm@28760: \item @{text "@{goals}"} prints the current \emph{dynamic} goal wenzelm@27043: state. This is mainly for support of tactic-emulation scripts wenzelm@28749: within Isar. Presentation of goal states does not conform to the wenzelm@28749: idea of human-readable proof documents! wenzelm@27043: wenzelm@28749: When explaining proofs in detail it is usually better to spell out wenzelm@28749: the reasoning via proper Isar proof commands, instead of peeking at wenzelm@28749: the internal machine configuration. wenzelm@27043: wenzelm@28760: \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but wenzelm@27043: does not print the main goal. wenzelm@27043: wenzelm@28760: \item @{text "@{prf a\<^sub>1 \ a\<^sub>n}"} prints the (compact) proof terms wenzelm@28749: corresponding to the theorems @{text "a\<^sub>1 \ a\<^sub>n"}. Note that this wenzelm@28749: requires proof terms to be switched on for the current logic wenzelm@28749: session. wenzelm@27043: wenzelm@28760: \item @{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \ wenzelm@28760: a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays wenzelm@28760: information omitted in the compact proof term, which is denoted by wenzelm@28760: ``@{text _}'' placeholders there. wenzelm@27043: wenzelm@46261: \item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type wenzelm@46261: s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value, wenzelm@46261: infix operator, type, and structure, respectively. The source is wenzelm@46261: printed verbatim. wenzelm@27043: wenzelm@40801: \item @{text "@{file path}"} checks that @{text "path"} refers to a wenzelm@40801: file (or directory) and prints it verbatim. wenzelm@40801: wenzelm@54705: \item @{text "@{file_unchecked path}"} is like @{text "@{file wenzelm@54705: path}"}, but does not check the existence of the @{text "path"} wenzelm@54705: within the file-system. wenzelm@54705: wenzelm@54702: \item @{text "@{url name}"} produces markup for the given URL, which wenzelm@54702: results in an active hyperlink within the text. wenzelm@54702: wenzelm@28760: \end{description} wenzelm@28749: *} wenzelm@27043: wenzelm@28749: wenzelm@42936: subsection {* Styled antiquotations *} wenzelm@28749: haftmann@32891: text {* The antiquotations @{text thm}, @{text prop} and @{text haftmann@32891: term} admit an extra \emph{style} specification to modify the haftmann@32891: printed result. A style is specified by a name with a possibly haftmann@32891: empty number of arguments; multiple styles can be sequenced with haftmann@32891: commas. The following standard styles are available: wenzelm@27043: wenzelm@28760: \begin{description} wenzelm@27043: wenzelm@28760: \item @{text lhs} extracts the first argument of any application wenzelm@28749: form with at least two arguments --- typically meta-level or wenzelm@27043: object-level equality, or any other binary relation. wenzelm@27043: wenzelm@28760: \item @{text rhs} is like @{text lhs}, but extracts the second wenzelm@27043: argument. wenzelm@27043: wenzelm@28760: \item @{text "concl"} extracts the conclusion @{text C} from a rule wenzelm@27043: in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"}. wenzelm@27043: haftmann@32891: \item @{text "prem"} @{text n} extract premise number haftmann@32891: @{text "n"} from from a rule in Horn-clause wenzelm@28760: normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} wenzelm@27043: wenzelm@28760: \end{description} wenzelm@28749: *} wenzelm@27043: wenzelm@28749: wenzelm@42936: subsection {* General options *} wenzelm@28749: wenzelm@28749: text {* The following options are available to tune the printed output wenzelm@54346: of antiquotations. Note that many of these coincide with system and wenzelm@54346: configuration options of the same names. wenzelm@27043: wenzelm@28760: \begin{description} wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def show_types}~@{text "= bool"} and wenzelm@30397: @{antiquotation_option_def show_sorts}~@{text "= bool"} control wenzelm@30397: printing of explicit type and sort constraints. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def show_structs}~@{text "= bool"} wenzelm@30397: controls printing of implicit structures. wenzelm@27043: wenzelm@40879: \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"} wenzelm@40879: controls folding of abbreviations. wenzelm@40879: wenzelm@42669: \item @{antiquotation_option_def names_long}~@{text "= bool"} forces wenzelm@30397: names of types and constants etc.\ to be printed in their fully wenzelm@30397: qualified internal form. wenzelm@27043: wenzelm@42669: \item @{antiquotation_option_def names_short}~@{text "= bool"} wenzelm@30397: forces names of types and constants etc.\ to be printed unqualified. wenzelm@30397: Note that internalizing the output again in the current context may wenzelm@30397: well yield a different result. wenzelm@27043: wenzelm@42669: \item @{antiquotation_option_def names_unique}~@{text "= bool"} wenzelm@30397: determines whether the printed version of qualified names should be wenzelm@30397: made sufficiently long to avoid overlap with names declared further wenzelm@30397: back. Set to @{text false} for more concise output. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def eta_contract}~@{text "= bool"} wenzelm@30397: prints terms in @{text \}-contracted form. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def display}~@{text "= bool"} indicates wenzelm@30397: if the text is to be output as multi-line ``display material'', wenzelm@30397: rather than a small piece of text without line breaks (which is the wenzelm@30397: default). wenzelm@27043: wenzelm@28749: In this mode the embedded entities are printed in the same style as wenzelm@28749: the main theory text. wenzelm@28749: wenzelm@30397: \item @{antiquotation_option_def break}~@{text "= bool"} controls wenzelm@30397: line breaks in non-display material. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates wenzelm@30397: if the output should be enclosed in double quotes. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text wenzelm@30397: name} to the print mode to be used for presentation. Note that the wenzelm@30397: standard setup for {\LaTeX} output is already present by default, wenzelm@30397: including the modes @{text latex} and @{text xsymbols}. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def margin}~@{text "= nat"} and wenzelm@30397: @{antiquotation_option_def indent}~@{text "= nat"} change the margin wenzelm@30397: or indentation for pretty printing of display material. wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def goals_limit}~@{text "= nat"} wenzelm@51960: determines the maximum number of subgoals to be printed (for goal-based wenzelm@30397: antiquotation). wenzelm@27043: wenzelm@30397: \item @{antiquotation_option_def source}~@{text "= bool"} prints the wenzelm@30397: original source text of the antiquotation arguments, rather than its wenzelm@30397: internal representation. Note that formal checking of wenzelm@30397: @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still wenzelm@30397: enabled; use the @{antiquotation "text"} antiquotation for unchecked wenzelm@30397: output. wenzelm@28749: wenzelm@28749: Regular @{text "term"} and @{text "typ"} antiquotations with @{text wenzelm@28749: "source = false"} involve a full round-trip from the original source wenzelm@28749: to an internalized logical entity back to a source form, according wenzelm@28749: to the syntax of the current context. Thus the printed output is wenzelm@28749: not under direct control of the author, it may even fluctuate a bit wenzelm@28749: as the underlying theory is changed later on. wenzelm@28749: wenzelm@42626: In contrast, @{antiquotation_option source}~@{text "= true"} wenzelm@30397: admits direct printing of the given source text, with the desirable wenzelm@30397: well-formedness check in the background, but without modification of wenzelm@30397: the printed text. wenzelm@28749: wenzelm@28760: \end{description} wenzelm@27043: wenzelm@27043: For boolean flags, ``@{text "name = true"}'' may be abbreviated as wenzelm@27043: ``@{text name}''. All of the above flags are disabled by default, wenzelm@51057: unless changed specifically for a logic session in the corresponding wenzelm@51057: @{verbatim "ROOT"} file. *} wenzelm@27043: wenzelm@27043: wenzelm@28750: section {* Markup via command tags \label{sec:tags} *} wenzelm@27043: wenzelm@28750: text {* Each Isabelle/Isar command may be decorated by additional wenzelm@28750: presentation tags, to indicate some modification in the way it is wenzelm@28750: printed in the document. wenzelm@27043: wenzelm@42596: @{rail " wenzelm@42596: @{syntax_def tags}: ( tag * ) wenzelm@27043: ; wenzelm@42596: tag: '%' (@{syntax ident} | @{syntax string}) wenzelm@42596: "} wenzelm@27043: wenzelm@28750: Some tags are pre-declared for certain classes of commands, serving wenzelm@28750: as default markup if no tags are given in the text: wenzelm@27043: wenzelm@28750: \medskip wenzelm@27043: \begin{tabular}{ll} wenzelm@27043: @{text "theory"} & theory begin/end \\ wenzelm@27043: @{text "proof"} & all proof commands \\ wenzelm@27043: @{text "ML"} & all commands involving ML code \\ wenzelm@27043: \end{tabular} wenzelm@27043: wenzelm@28750: \medskip The Isabelle document preparation system wenzelm@28750: \cite{isabelle-sys} allows tagged command regions to be presented wenzelm@27043: specifically, e.g.\ to fold proof texts, or drop parts of the text wenzelm@27043: completely. wenzelm@27043: wenzelm@28750: For example ``@{command "by"}~@{text "%invisible auto"}'' causes wenzelm@28750: that piece of proof to be treated as @{text invisible} instead of wenzelm@28750: @{text "proof"} (the default), which may be shown or hidden wenzelm@27043: depending on the document setup. In contrast, ``@{command wenzelm@28750: "by"}~@{text "%visible auto"}'' forces this text to be shown wenzelm@27043: invariably. wenzelm@27043: wenzelm@27043: Explicit tag specifications within a proof apply to all subsequent wenzelm@27043: commands of the same level of nesting. For example, ``@{command wenzelm@28750: "proof"}~@{text "%visible \"}~@{command "qed"}'' forces the whole wenzelm@28750: sub-proof to be typeset as @{text visible} (unless some of its parts wenzelm@28750: are tagged differently). wenzelm@28750: wenzelm@28750: \medskip Command tags merely produce certain markup environments for wenzelm@28750: type-setting. The meaning of these is determined by {\LaTeX} wenzelm@40800: macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or wenzelm@28750: by the document author. The Isabelle document preparation tools wenzelm@28750: also provide some high-level options to specify the meaning of wenzelm@28750: arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding wenzelm@28750: parts of the text. Logic sessions may also specify ``document wenzelm@28750: versions'', where given tags are interpreted in some particular way. wenzelm@28750: Again see \cite{isabelle-sys} for further details. wenzelm@27043: *} wenzelm@27043: wenzelm@27043: wenzelm@42658: section {* Railroad diagrams *} wenzelm@42658: wenzelm@42658: text {* wenzelm@42658: \begin{matharray}{rcl} wenzelm@42658: @{antiquotation_def "rail"} & : & @{text antiquotation} \\ wenzelm@42658: \end{matharray} wenzelm@42658: wenzelm@42658: @{rail "'rail' string"} wenzelm@42658: wenzelm@42658: The @{antiquotation rail} antiquotation allows to include syntax wenzelm@42658: diagrams into Isabelle documents. {\LaTeX} requires the style file wenzelm@53982: @{file "~~/lib/texinputs/pdfsetup.sty"}, which can be used via wenzelm@42658: @{verbatim "\\usepackage{pdfsetup}"} in @{verbatim "root.tex"}, for wenzelm@42658: example. wenzelm@42658: wenzelm@42658: The rail specification language is quoted here as Isabelle @{syntax wenzelm@42658: string}; it has its own grammar given below. wenzelm@42658: wenzelm@42658: @{rail " wenzelm@42658: rule? + ';' wenzelm@42658: ; wenzelm@42658: rule: ((identifier | @{syntax antiquotation}) ':')? body wenzelm@42658: ; wenzelm@42658: body: concatenation + '|' wenzelm@42658: ; wenzelm@42658: concatenation: ((atom '?'?) +) (('*' | '+') atom?)? wenzelm@42658: ; wenzelm@42658: atom: '(' body? ')' | identifier | wenzelm@42658: '@'? (string | @{syntax antiquotation}) | wenzelm@42658: '\\\\\\\\' wenzelm@42658: "} wenzelm@42658: wenzelm@42658: The lexical syntax of @{text "identifier"} coincides with that of wenzelm@42658: @{syntax ident} in regular Isabelle syntax, but @{text string} uses wenzelm@42658: single quotes instead of double quotes of the standard @{syntax wenzelm@42658: string} category, to avoid extra escapes. wenzelm@42658: wenzelm@42658: Each @{text rule} defines a formal language (with optional name), wenzelm@42658: using a notation that is similar to EBNF or regular expressions with wenzelm@42658: recursion. The meaning and visual appearance of these rail language wenzelm@42658: elements is illustrated by the following representative examples. wenzelm@42658: wenzelm@42658: \begin{itemize} wenzelm@42658: wenzelm@42658: \item Empty @{verbatim "()"} wenzelm@42658: wenzelm@42658: @{rail "()"} wenzelm@42658: wenzelm@42658: \item Nonterminal @{verbatim "A"} wenzelm@42658: wenzelm@42658: @{rail "A"} wenzelm@42658: wenzelm@42658: \item Nonterminal via Isabelle antiquotation wenzelm@42658: @{verbatim "@{syntax method}"} wenzelm@42658: wenzelm@42658: @{rail "@{syntax method}"} wenzelm@42658: wenzelm@42658: \item Terminal @{verbatim "'xyz'"} wenzelm@42658: wenzelm@42658: @{rail "'xyz'"} wenzelm@42658: wenzelm@42658: \item Terminal in keyword style @{verbatim "@'xyz'"} wenzelm@42658: wenzelm@42658: @{rail "@'xyz'"} wenzelm@42658: wenzelm@42658: \item Terminal via Isabelle antiquotation wenzelm@42658: @{verbatim "@@{method rule}"} wenzelm@42658: wenzelm@42658: @{rail "@@{method rule}"} wenzelm@42658: wenzelm@42658: \item Concatenation @{verbatim "A B C"} wenzelm@42658: wenzelm@42658: @{rail "A B C"} wenzelm@42658: wenzelm@42658: \item Linebreak @{verbatim "\\\\"} inside wenzelm@42658: concatenation\footnote{Strictly speaking, this is only a single wenzelm@42658: backslash, but the enclosing @{syntax string} syntax requires a wenzelm@42658: second one for escaping.} @{verbatim "A B C \\\\ D E F"} wenzelm@42658: wenzelm@42658: @{rail "A B C \\ D E F"} wenzelm@42658: wenzelm@42658: \item Variants @{verbatim "A | B | C"} wenzelm@42658: wenzelm@42658: @{rail "A | B | C"} wenzelm@42658: wenzelm@42658: \item Option @{verbatim "A ?"} wenzelm@42658: wenzelm@42658: @{rail "A ?"} wenzelm@42658: wenzelm@42658: \item Repetition @{verbatim "A *"} wenzelm@42658: wenzelm@42658: @{rail "A *"} wenzelm@42658: wenzelm@42658: \item Repetition with separator @{verbatim "A * sep"} wenzelm@42658: wenzelm@42658: @{rail "A * sep"} wenzelm@42658: wenzelm@42658: \item Strict repetition @{verbatim "A +"} wenzelm@42658: wenzelm@42658: @{rail "A +"} wenzelm@42658: wenzelm@42658: \item Strict repetition with separator @{verbatim "A + sep"} wenzelm@42658: wenzelm@42658: @{rail "A + sep"} wenzelm@42658: wenzelm@42658: \end{itemize} wenzelm@42658: *} wenzelm@42658: wenzelm@42658: wenzelm@27043: section {* Draft presentation *} wenzelm@27043: wenzelm@27043: text {* wenzelm@27043: \begin{matharray}{rcl} wenzelm@28761: @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \"} \\ wenzelm@27043: \end{matharray} wenzelm@27043: wenzelm@42596: @{rail " wenzelm@52549: @@{command display_drafts} (@{syntax name} +) wenzelm@42596: wenzelm@42596: "} wenzelm@27043: wenzelm@28760: \begin{description} wenzelm@27043: wenzelm@52549: \item @{command "display_drafts"}~@{text paths} performs simple output of a wenzelm@52549: given list of raw source files. Only those symbols that do not require wenzelm@52549: additional {\LaTeX} packages are displayed properly, everything else is left wenzelm@52549: verbatim. wenzelm@27043: wenzelm@28760: \end{description} wenzelm@27043: *} wenzelm@27043: wenzelm@27043: end