Quelle  Document_Preparation.thy

(*:maxLineLen=78:*)

theory Document_Preparation
  imports Main Base
begin

chapter ‹Document preparation \label{ch:document-prep}›

text ‹
  Isabelle/Isar provides a simple document preparation system based on
  {PDF-\LaTeX}, with support for hyperlinks and bookmarks within that format.
  This allows to produce papers, books, theses etc.\ from Isabelle theory
  sources.
 
  {\LaTeX} output is generated while processing a 🪙‹session› i
  explained in the 🪙‹The Isabelle System Manual› 🍋‹"isabelle-system"›.
  The main Isabelle tools to get started with document preparation are
  @{tool_ref mkroot} and @{tool_ref build}.

  The classic Isabelle/HOL tutorial 🍋‹"isabelle-hol-book"› also explains
  some aspects of theory presentation.
›


section ‹Markup commands \label{sec:markup}›

text ‹
  \begin{matharray}{rcl}
  @{command_def "chapter"} & : & ‹any → any› \
    @{command_def "section"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "subsection"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "subsubsection"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "paragraph"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "subparagraph"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "text"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "txt"} & : & ‹any → any› java.lang.NullPointerException
    @{command_def "text_raw"} & : & ‹any → any› java.lang.NullPointerException
  \end{matharray}

  Markup commands provide a structured way to insert text into the document
  generated from a theory. Each markup command takes a single @{syntax text}
  argument, which is passed as argument to a corresponding {\LaTeX} macro. The
  default macros provided by 🍋‹~~/lib/texinputs/isabelle.sty› can be
  redefined according to the needs of the underlying document and {\LaTeX}
  styles.

  Note that formal comments (\secref{sec:comments}) are similar to markup
  commands, but have a different status within Isabelle/Isar syntax.

  🪙‹
  (@@{command chapter} | @@{command section} | @@{command subsection} |
  @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph})
  @{syntax text} ';'? |
  (@@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
  ›

    🪙 @{command chapter}, @{command section}, @{command subsection} etc.\ mark
    section headings within the theory source. This works in any context, even
    before the initial @{command theory} command. The corresponding {\LaTeX}
    macros are 🍋‹\isamarkupchapter›, 🍋‹\isamarkupsection›,
    🍋‹\isamarkupsubsection› etc.java.lang.NullPointerException

    🪙 @{command text} and @{command txt} specify paragraphs of plain text.
    This corresponds to a {\LaTeX} environment 🍋‹\begin{isamarkuptext}› ‹…›
    🍋‹\end{isamarkuptext}› etc.

    🪙 @{command text_raw} is similar to @{command text}, but without any
    surrounding markup environment. This allows to inject arbitrary {\LaTeX}
    source into the generated document.

  All text passed to any of the above markup commands may refer to formal
  entities via 🪙‹document antiquotations›, see also \secref{sec:antiq}. These
  are interpreted in the present theory or proof context.

  🪙
  The proof markup commands closely resemble those for theory specifications,
  but have a different formal status and produce different {\LaTeX} macros.
›


section ‹Document antiquotations \label{sec:antiq}›

text ‹
  \begin{matharray}{rcl}
  @{antiquotation_def "theory"} & : & ‹antiquotation› \
    @{antiquotation_def "thm"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "lemma"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "prop"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "term"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def term_type} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def typeof} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def const} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def abbrev} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def typ} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def type} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def class} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def locale} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def bundle} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "text"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def goals} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def subgoals} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def prf} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def full_prf} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_text} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_def} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_ref} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_infix} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_infix_def} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_infix_ref} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_type} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_type_def} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_type_ref} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_structure} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_structure_def} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_structure_ref} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_functor} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_functor_def} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def ML_functor_ref} & : & ‹antiquotation› java.lang.NullPointerException
  \end{matharray}

  \begin{matharray}{rcl}
    @{antiquotation_def emph} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def bold} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def verbatim} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def bash_function} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def system_option} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def session} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "file"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "url"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "cite"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "nocite"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "citet"} & : & ‹antiquotation› java.lang.NullPointerException
    @{antiquotation_def "citep"} & : & ‹antiquotation› java.lang.NullPointerException
    @{command_def "print_antiquotations"}‹🪙*› & : & ‹context →› java.lang.NullPointerException
  \end{matharray}

  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 🪙‹document antiquotations›.

  For example, embedding 🍋‹@{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.

  🪙
  Antiquotations are in general written as
  🍋‹@{›\<open>name›~🍋‹[›\<open>options›🍋‹]›~‹arguments›\<^verbatim>‹}›. The short form
  🍋‹\\›\<^verbatim>‹🚫close>‹name›\<^verbatim>‹>›\<open>‹argument_content›\<close> (without surrounding 🍋‹@{›\<open>…›🍋‹}›)
  works for a single argument that is a cartouche. A cartouche without special
  decoration is equivalent to 🍋‹🪙›\<open>‹argument_content›\<close>, which is
  equivalent to 🍋‹@{cartouche›~‹‹argument_content›\🍋‹}›. The special name
  @{antiquotation_def cartouche} is defined in the context: Isabelle/Pure
  introduces that as an alias to @{antiquotation_ref text} (see below).
  Consequently, ‹‹foo_bar + baz ≤ bazar›\text
  (unchecked). A control symbol 🍋‹\\›\<^verbatim>‹🚫close>‹name›\🍋‹>› within the body text, but
  without a subsequent cartouche, is equivalent to 🍋‹@{›\‹name›\🍋‹}›.
 
  \begingroup
  \def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
  🪙‹
  @{syntax_def antiquotation}:
  '@{' antiquotation_body '}' |
  '🪙' @{syntax_ref name} '>' @{syntax_ref cartouche} |
  @{syntax_ref cartouche}
  ;
  options: '[' (option * ',') ']'
  ;
  option: @{syntax name} | @{syntax name} '=' @{syntax name}
  ;
  ›
  \endgroup
 
  Note that the syntax of antiquotations may 🪙‹not› include source comments
  \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)

  %% FIXME less monolithic presentation, move to individual sections!?
  🪙‹
  @{syntax_def antiquotation_body}:
  (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
  options @{syntax text} |
  @@{antiquotation theory} options @{syntax embedded} |
  @@{antiquotation thm} options styles @{syntax thms} |
  @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
  @@{antiquotation prop} options styles @{syntax prop} |
  @@{antiquotation term} options styles @{syntax term} |
  @@{antiquotation (HOL) value} options styles @{syntax term} |
  @@{antiquotation term_type} options styles @{syntax term} |
  @@{antiquotation typeof} options styles @{syntax term} |
  @@{antiquotation const} options @{syntax term} |
  @@{antiquotation abbrev} options @{syntax term} |
  @@{antiquotation typ} options @{syntax type} |
  @@{antiquotation type} options @{syntax embedded} |
  @@{antiquotation class} options @{syntax embedded} |
  @@{antiquotation locale} options @{syntax embedded} |
  @@{antiquotation bundle} options @{syntax embedded} |
  (@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
  options @{syntax name}
  ;
  @{syntax antiquotation}:
  @@{antiquotation goals} options |
  @@{antiquotation subgoals} options |
  @@{antiquotation prf} options @{syntax thms} |
  @@{antiquotation full_prf} options @{syntax thms} |
  @@{antiquotation ML_text} options @{syntax text} |
  @@{antiquotation ML} options @{syntax text} |
  @@{antiquotation ML_infix} options @{syntax text} |
  @@{antiquotation ML_type} options @{syntax typeargs} @{syntax text} |
  @@{antiquotation ML_structure} options @{syntax text} |
  @@{antiquotation ML_functor} options @{syntax text} |
  @@{antiquotation emph} options @{syntax text} |
  @@{antiquotation bold} options @{syntax text} |
  @@{antiquotation verbatim} options @{syntax text} |
  @@{antiquotation bash_function} options @{syntax embedded} |
  @@{antiquotation system_option} options @{syntax embedded} |
  @@{antiquotation session} options @{syntax embedded} |
  @@{antiquotation path} options @{syntax embedded} |
  @@{antiquotation "file"} options @{syntax name} |
  @@{antiquotation dir} options @{syntax name} |
  @@{antiquotation url} options @{syntax embedded} |
  (@@{antiquotation cite} | @@{antiquotation nocite} |
  @@{antiquotation citet} | @@{antiquotation citep}) @{syntax embedded}
  ;
  styles: '(' (style + ',') ')'
  ;
  style: (@{syntax name} +)
  ;
  @@{command print_antiquotations} ('!'?)
  ›

  🪙 ‹@{text s}› prints uninterpreted source text ‹s›, i.e.\ inner syntax. This
  is particularly useful to print portions of text according to the Isabelle
  document style, without demanding well-formedness, e.g.\ small pieces of
  terms that should not be parsed or type-checked yet.

  It is also possible to write this in the short form ‹‹s›\› without any
  further decoration.

  🪙 ‹@{theory_text s}› prints uninterpreted theory source text ‹s›, i.e.java.lang.NullPointerException
  outer syntax with command keywords and other tokens.

  🪙 ‹@{theory A}› prints the session-qualified theory name ‹A›, which is
  guaranteed to refer to a valid ancestor theory in the current context.

  🪙 ‹@{thm a🪙1 … a🪙n}› prints theorems ‹a🪙1 … a🪙n›. Full fact expressions are
  allowed here, including attributes (\secref{sec:syn-att}).

  🪙 ‹@{prop φ}› prints a well-typed proposition ‹φ›.

  🪙 ‹@{lemma φ by m}› proves a well-typed proposition ‹φ› by method ‹m› and
  prints the original ‹φ›.

  🪙 ‹@{term t}› prints a well-typed term ‹t›.
  
  🪙 ‹@{value t}› evaluates a term ‹t› and prints its result, see also
  @{command_ref (HOL) value}.

  🪙 ‹@{term_type t}› prints a well-typed term ‹t› annotated with its type.

  🪙 ‹@{typeof t}› prints the type of a well-typed term ‹t›.

  🪙 ‹@{const c}› prints a logical or syntactic constant ‹c›.
  
  🪙 ‹@{abbrev c x🪙1 … x🪙n}› prints a constant abbreviation ‹c x🪙1 … x🪙n ≡ rhs›
  as defined in the current context.

  🪙 ‹@{typ τ}› prints a well-formed type ‹τ›.

  🪙 ‹@{type κ}› prints a (logical or syntactic) type constructor ‹κ›.

  🪙 ‹@{class c}› prints a class ‹c›.

  🪙 ‹@{locale c}› prints a locale ‹c›.

  🪙 ‹@{bundle c}› prints a bundle ‹c›.

  🪙 ‹@{command name}›, ‹@{method name}›, ‹@{attribute name}› print checked
  entities of the Isar language.

  🪙 ‹@{goals}› prints the current 🪙‹dynamic› goal state. This is mainly for
  support of tactic-emulation scripts within Isar. Presentation of goal states
  does not conform to the idea of human-readable proof documents!

  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.
  
  🪙 ‹@{subgoals}› is similar to ‹@{goals}›, but does not print the main goal.
  
  🪙 ‹@{prf a🪙1 … a🪙n}› prints the (compact) proof terms corresponding to the
  theorems ‹a🪙1 … a🪙n›. Note that this requires proof terms to be switched on
  for the current logic session.
  
  🪙 ‹@{full_prf a🪙1 … a🪙n}› is like ‹@{prf a🪙1 … a🪙n}›, but prints the full
  proof terms, i.e.\ also displays information omitted in the compact proof
  term, which is denoted by ``‹_›'' placeholders there.

  🪙 ‹@{ML_text s}› prints ML text verbatim: only the token language is
  checked.

  🪙 ‹@{ML s}›, ‹@{ML_infix s}›, ‹@{ML_type s}›, ‹@{ML_structure s}›, and
  ‹@{ML_functor s}› check text ‹s› as ML value, infix operator, type,
  exception, structure, and functor respectively. The source is printed
  verbatim. The variants ‹@{ML_def s}› and ‹@{ML_ref s}› etc. maintain the
  document index: ``def'' means to make a bold entry, ``ref'' means to make a
  regular entry.

  There are two forms for type constructors, with or without separate type
  arguments: this impacts only the index entry. For example, ‹@{ML_type_ref
  ‹'a list›}›
  letter ``a''), but ‹@{ML_type_ref 'a ‹list›}› makes an entry for the
  constructor name ``‹list›''.

  🪙 ‹@{emph s}› prints document source recursively, with {\LaTeX} markup
  🍋‹\emph{›\<open>…›🍋‹}›.

  🪙 ‹@{bold s}› prints document source recursively, with {\LaTeX} markup
  🍋‹\textbf{›\<open>…›🍋‹}›.

  🪙 ‹@{verbatim s}› prints uninterpreted source text literally as ASCII
  characters, using some type-writer font style.

  🪙 ‹@{bash_function name}› prints the given GNU bash function verbatim. The
  name is checked wrt.\ the Isabelle system environment 🍋‹"isabelle-system"›.

  🪙 ‹@{system_option name}› prints the given system option verbatim. The name
  is checked wrt.\ cumulative 🍋‹etc/options› of all Isabelle components,
  notably 🍋‹~~/etc/options›.

  🪙 ‹@{session name}› prints given session name verbatim. The name is checked
  wrt.\ the dependencies of the current session.

  🪙 ‹@{path name}› prints the file-system path name verbatim.

  🪙 ‹@{file name}› is like ‹@{path name}›, but ensures that ‹name› refers to a
  plain file.

  🪙 ‹@{dir name}› is like ‹@{path name}›, but ensures that ‹name› refers to a
  directory.

  🪙 ‹@{url name}› produces markup for the given URL, which results in an
  active hyperlink within the text.

  🪙 ‹@{cite arg}› produces the Bib{\TeX} citation macro 🍋‹\cite[...]{...}›
  with its optional and mandatory argument. The analogous 🍋‹\nocite›, and the
  🍋‹\citet› and 🍋‹\citep› variants from the 🍋‹natbib›
  package🪙‹🪙‹https://ctan.org/pkg/natbib›\
  The argument syntax is uniform for all variants and is usually presented in
  control-symbol-cartouche form: ‹🍋‹arg›\syntax of the
  nested argument language is defined as follows: 🪙‹arg: (embedded
  @'in')? (name + @'and') 🍋 (@'using' name)?›

  Here the embedded text is free-form {\LaTeX}, which becomes the optional
  argument of the 🍋‹\cite› macro. The named items are Bib{\TeX} database
  entries and become the mandatory argument (separated by comma). The optional
  part ``🪙‹using name›'' specifies an alternative {\LaTeX} macro name.

  🪙 @{command "print_antiquotations"} prints all document antiquotations that
  are defined in the current context; the ``‹!›'' option indicates extra
  verbosity.
›


subsection ‹Styled antiquotations›

text ‹
  The antiquotations ‹thm›,
  specification to modify the printed result. A style is specified by a name
  with a possibly empty number of arguments; multiple styles can be sequenced
  with commas. The following standard styles are available:

  🪙 ‹lhs› extracts the first argument of any application form with at least
  two arguments --- typically meta-level or object-level equality, or any
  other binary relation.
  
  🪙 ‹rhs› is like ‹lhs›, but extracts the second argument.
  
  🪙 ‹concl› extracts the conclusion ‹C› from a rule in Horn-clause normal form
  ‹A🪙1 ==> … A🪙n ==> C›.
  
  🪙 ‹prem› ‹n› extract premise number ‹n› from from a rule in Horn-clause
  normal form ‹A🪙1 ==> … A🪙n ==> C›.
›


subsection ‹General options›

text ‹
  The following options are available to tune the printed output of
  antiquotations. Note that many of these coincide with system and
  configuration options of the same names.
 
  🪙 @{antiquotation_option_def show_types}~‹= bool› a
    @{antiquotation_option_def show_sorts}~‹= bool› control printing of
    explicit type and sort constraints.

    🪙 @{antiquotation_option_def show_structs}~‹= bool› controls printing of
    implicit structures.

    🪙 @{antiquotation_option_def show_abbrevs}~‹= bool› controls folding of
    abbreviations.

    🪙 @{antiquotation_option_def names_long}~‹= bool› forces names of types
    and constants etc.\ to be printed in their fully qualified internal form.

    🪙 @{antiquotation_option_def names_short}~‹= bool› forces names of types
    and constants etc.\ to be printed unqualified. Note that internalizing the
    output again in the current context may well yield a different result.

    🪙 @{antiquotation_option_def names_unique}~‹= bool› determines whether the
    printed version of qualified names should be made sufficiently long to
    avoid overlap with names declared further back. Set to ‹false› for more
    concise output.

    🪙 @{antiquotation_option_def eta_contract}~‹= bool› prints terms in
    ‹🪙›-contracted form.

    🪙 @{antiquotation_option_def display}~‹= bool› indicates if the text is to
    be 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.

    🪙 @{antiquotation_option_def break}~‹= bool› controls line breaks in
    non-display material.

    🪙 @{antiquotation_option_def cartouche}~‹= bool› indicates if the output
    should be delimited as cartouche.

    🪙 @{antiquotation_option_def quotes}~‹= bool› indicates if the output
    should be delimited via double quotes (option @{antiquotation_option
    cartouche} takes precedence). Note that the Isabelle {\LaTeX} styles may
    suppress quotes on their own account.

    🪙 @{antiquotation_option_def mode}~‹= name› adds ‹name› to the print mode
    to be used for presentation. Note that the standard setup for {\LaTeX}
    output is already present by default, with mode ``‹latex›''.

    🪙 @{antiquotation_option_def margin}~‹= nat› and
    @{antiquotation_option_def indent}~‹= nat› change the margin or
    indentation for pretty printing of display material.

    🪙 @{antiquotation_option_def goals_limit}~‹= nat› determines the maximum
    number of subgoals to be printed (for goal-based antiquotation).

    🪙 @{antiquotation_option_def 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 ‹term› and ‹typ› antiquotations with ‹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, @{antiquotation_option 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.

    Cartouche delimiters of the argument are stripped for antiquotations that
    are internally categorized as ``embedded''.

    🪙 @{antiquotation_option_def source_cartouche} is like
    @{antiquotation_option source}, but cartouche delimiters are always
    preserved in the output.

  For Boolean flags, ``‹name = true›'' may be abbreviated as ``‹name›''. All
  of the above flags are disabled by default, unless changed specifically for
  a logic session in the corresponding 🍋‹ROOT› file.
›


section ‹Markdown-like text structure›

text ‹
  The markup commands @{command_ref text}, @{command_ref txt}, @{command_ref
  text_raw} (\secref{sec:markup}) consist of plain text. Its internal
  structure consists of paragraphs and (nested) lists, using special Isabelle
  symbols and some rules for indentation and blank lines. This quasi-visual
  format resembles 🪙‹Markdown›\<
  complexity of that notation is avoided.

  This is a summary of the main principles of minimal Markdown in Isabelle:

    🪙 List items start with the following markers
      🪙[itemize:] 🍋‹🪙›
      🪙[enumerate:] 🍋‹🪙›
      🪙[description:] 🍋‹🪙›

    🪙 Adjacent list items with same indentation and same marker are grouped
    into a single list.

    🪙 Singleton blank lines separate paragraphs.

    🪙 Multiple blank lines escape from the current list hierarchy.

  Notable differences to official Markdown:

    🪙 Indentation of list items needs to match exactly.

    🪙 Indentation is unlimited (official Markdown interprets four spaces as
    block quote).

    🪙 List items always consist of paragraphs --- there is no notion of
    ``tight'' list.

    🪙 Section headings are expressed via Isar document markup commands
    (\secref{sec:markup}).

    🪙 URLs, font styles, other special content is expressed via antiquotations
    (\secref{sec:antiq}), usually with proper nesting of sub-languages via
    text cartouches.
›


section ‹Document markers and command tags \label{sec:document-markers}›

text ‹
  \emph{Document markers} are formal comments of the form ‹🍋‹marker_body›\›
  (using the control symbol 🍋‹🍋›) and may occur anywhere within the
  outer syntax of a command: the inner syntax of a marker body resembles that
  for attributes (\secref{sec:syn-att}). In contrast, \emph{Command tags} may
  only occur after a command keyword and are treated as special markers as
  explained below.

  🪙‹
  @{syntax_def marker}: '🍋' @{syntax cartouche}
  ;
  @{syntax_def marker_body}: (@{syntax name} @{syntax args} * ',')
  ;
  @{syntax_def tags}: tag*
  ;
  tag: '%' (@{syntax short_ident} | @{syntax string})
  ›

  Document markers are stripped from the document output, but surrounding
  white-space is preserved: e.g.\ a marker at the end of a line does not
  affect the subsequent line break. Markers operate within the semantic
  presentation context of a command, and may modify it to change the overall
  appearance of a command span (e.g.\ by adding tags).

  Each document marker has its own syntax defined in the theory context; the
  following markers are predefined in Isabelle/Pure:

  🪙‹
  (@@{document_marker_def title} |
  @@{document_marker_def creator} |
  @@{document_marker_def contributor} |
  @@{document_marker_def date} |
  @@{document_marker_def license} |
  @@{document_marker_def description}) @{syntax embedded}
  ;
  @@{document_marker_def tag} (scope?) @{syntax name}
  ;
  scope: '(' ('proof' | 'command') ')'
  ›

    🪙 ‹🍋‹title arg›\›, ‹🍋‹creator arg›\›, ‹🍋‹contributor arg›\›, ‹🍋‹date arg›\›,
    ‹🍋‹license arg›\›, and ‹🍋‹description arg›\› produce markup in the PIDE
    document, without any immediate effect on typesetting. This vocabulary is
    taken from the Dublin Core Metadata
    Initiative🪙‹🪙‹https://www.dublincore.org/specifications/dublin-core/dcmi-terms›\›.
    The argument is an uninterpreted string, except for @{document_marker
    description}, which consists of words that are subject to spell-checking.

    🪙 ‹🍋‹tag name›\› updates the list of command tags in the presentation
    context: later declarations take precedence, so ‹🍋‹tag a, tag b, tag c›\›
    produces a reversed list. The default tags are given by the original
    🪙‹keywords› declaration of a command, and the system option
    @{system_option_ref document_tags}.

    The optional ‹scope› tells how far the tagging is applied to subsequent
    proof structure: ``🪙‹("proof")›'' means it applies to the following proof
    text, and ``🪙‹(command)›'' means it only applies to the current command.
    The default within a proof body is ``🪙‹("proof")›'', but for toplevel goal
    statements it is ``🪙‹(command)›''. Thus a ‹tag› marker for 🪙‹theorem›,
    🪙‹lemma› etc. does \emph{not} affect its proof by default.

    An old-style command tag 🍋‹%›\<open>name› is treated like a document marker
    ‹🍋‹tag (proof) name›\     document markers. The head of the resulting tags in the presentation
    context is turned into {\LaTeX} environments to modify the type-setting.
    The following tags are pre-declared for certain classes of commands, and
    serve as default markup for certain kinds of commands:

    🪙
    \begin{tabular}{ll}
      ‹document› & document markup commands java.lang.NullPointerException
      ‹theory› & theory begin/end java.lang.NullPointerException
      ‹proof› & all proof commands java.lang.NullPointerException
      ‹ML› & all commands involving ML code java.lang.NullPointerException
    \end{tabular}
    🪙

  The Isabelle document preparation system 🍋‹"isabelle-system"› allows
  tagged command regions to be presented specifically, e.g.\ to fold proof
  texts, or drop parts of the text completely.

  For example ``🪙‹by auto›~‹🍋‹tag invisible›\›'' causes that piece of proof to
  be treated as ‹invisible› instead of ‹proof› (the default), which may be
  shown or hidden depending on the document setup. In contrast, ``🪙‹by
  auto›~

  Explicit tag specifications within a proof apply to all subsequent commands
  of the same level of nesting. For example, ``🪙‹proof›~‹🍋‹tag invisible›
  …›~
  some of its parts are tagged differently).

  🪙
  Command tags merely produce certain markup environments for type-setting.
  The meaning of these is determined by {\LaTeX} macros, as defined in
  🍋‹~~/lib/texinputs/isabelle.sty› or by the document author. The Isabelle
  document preparation tools also provide some high-level options to specify
  the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
  corresponding parts of the text. Logic sessions may also specify ``document
  versions'', where given tags are interpreted in some particular way. Again
  see 🍋‹"isabelle-system"› for further details.
›


section ‹Railroad diagrams›

text ‹
  \begin{matharray}{rcl}
  @{antiquotation_def "rail"} & : & ‹antiquotation› \
  \end{matharray}

  🪙‹
  'rail' @{syntax text}
  ›

  The @{antiquotation rail} antiquotation allows to include syntax diagrams
  into Isabelle documents. {\LaTeX} requires the style file
  🍋‹~~/lib/texinputs/railsetup.sty›, which can be used via
  🍋‹\usepackage{railsetup}› in 🍋‹root.tex›, for example.

  The rail specification language is quoted here as Isabelle @{syntax string}
  or text @{syntax "cartouche"}; it has its own grammar given below.

  \begingroup
  \def\isasymnewline{\isatt{\isacharbackslash\isacharless newline\isachargreater}}
  🪙‹
  rule? + ';'
  ;
  rule: ((identifier | @{syntax antiquotation}) ':')? body
  ;
  body: concatenation + '|'
  ;
  concatenation: ((atom '?'?) +) (('*' | '+') atom?)?
  ;
  atom: '(' body? ')' | identifier |
  '@'? (string | @{syntax antiquotation}) |
  '🍋'
  ›
  \endgroup

  The lexical syntax of ‹identifier› coincides with that of @{syntax
  short_ident} in regular Isabelle syntax, but ‹string› uses single quotes
  instead of double quotes of the standard @{syntax string} category.

  Each ‹rule› defines a formal language (with optional name), using a notation
  that is similar to EBNF or regular expressions with recursion. The meaning
  and visual appearance of these rail language elements is illustrated by the
  following representative examples.

  🪙 Empty 🍋‹()›

  🪙‹()›

  🪙 Nonterminal 🍋‹A›

  🪙‹A›

  🪙 Nonterminal via Isabelle antiquotation 🍋‹@{syntax method}›

  🪙‹@{syntax method}›

  🪙 Terminal 🍋‹'xyz'›

  🪙‹'xyz'›

  🪙 Terminal in keyword style 🍋‹@'xyz'›

  🪙‹@'xyz'›

  🪙 Terminal via Isabelle antiquotation 🍋‹@@{method rule}›

  🪙‹@@{method rule}›

  🪙 Concatenation 🍋‹A B C›

  🪙‹A B C›

  🪙 Newline inside concatenation 🍋‹A B C 🍋 D E F›

  🪙‹A B C 🍋 D E F›

  🪙 Variants 🍋‹A | B | C›

  🪙‹A | B | C›

  🪙 Option 🍋‹A ?›

  🪙‹A ?›

  🪙 Repetition 🍋‹A *›

  🪙‹A *›

  🪙 Repetition with separator 🍋‹A * sep›

  🪙‹A * sep›

  🪙 Strict repetition 🍋‹A +›

  🪙‹A +›

  🪙 Strict repetition with separator 🍋‹A + sep›

  🪙‹A + sep›
›

end