
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 \<rightarrow> toplevel"} \\[0.5ex]
wenzelm@28761:     @{command_def "chapter"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761:     @{command_def "section"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761:     @{command_def "subsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761:     @{command_def "subsubsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761:     @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761:     @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
wenzelm@28761:     @{command_def "sect"} & : & @{text "proof \<rightarrow> proof"} \\
wenzelm@28761:     @{command_def "subsect"} & : & @{text "proof \<rightarrow> proof"} \\
wenzelm@28761:     @{command_def "subsubsect"} & : & @{text "proof \<rightarrow> proof"} \\
wenzelm@28761:     @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
wenzelm@28761:     @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> 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 "\<dots>"} @{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 "\<dots>"}~@{verbatim "*)"} nor verbatim
wenzelm@27043:   text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{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 \<dots> a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \<dots> 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 \<phi>}"} prints a well-typed proposition @{text
wenzelm@27043:   "\<phi>"}.
wenzelm@27043: 
wenzelm@28760:   \item @{text "@{lemma \<phi> by m}"} proves a well-typed proposition
wenzelm@28749:   @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
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 \<dots> x\<^sub>n}"} prints a constant abbreviation
wenzelm@28760:   @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
haftmann@39305: 
wenzelm@28760:   \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
haftmann@39305: 
wenzelm@39689:   \item @{text "@{type \<kappa>}"} prints a (logical or syntactic) type
wenzelm@39689:     constructor @{text "\<kappa>"}.
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 \<dots> a\<^sub>n}"} prints the (compact) proof terms
wenzelm@28749:   corresponding to the theorems @{text "a\<^sub>1 \<dots> 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 \<dots> a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \<dots>
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 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> 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 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> 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 \<eta>}-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 \<dots>"}~@{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 \<rightarrow>"} \\
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




