src/Doc/Isar_Ref/Document_Preparation.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59783 00b62aa9f430
child 59917 9830c944670f
permissions -rw-r--r--
tuned signature;
     1 theory Document_Preparation
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>Document preparation \label{ch:document-prep}\<close>
     6 
     7 text \<open>Isabelle/Isar provides a simple document preparation system
     8   based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
     9   within that format.  This allows to produce papers, books, theses
    10   etc.\ from Isabelle theory sources.
    11 
    12   {\LaTeX} output is generated while processing a \emph{session} in
    13   batch mode, as explained in the \emph{The Isabelle System Manual}
    14   @{cite "isabelle-sys"}.  The main Isabelle tools to get started with
    15   document preparation are @{tool_ref mkroot} and @{tool_ref build}.
    16 
    17   The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also
    18   explains some aspects of theory presentation.\<close>
    19 
    20 
    21 section \<open>Markup commands \label{sec:markup}\<close>
    22 
    23 text \<open>
    24   \begin{matharray}{rcl}
    25     @{command_def "chapter"} & : & @{text "any \<rightarrow> any"} \\
    26     @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
    27     @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
    28     @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
    29     @{command_def "text"} & : & @{text "any \<rightarrow> any"} \\
    30     @{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\
    31     @{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\
    32   \end{matharray}
    33 
    34   Markup commands provide a structured way to insert text into the
    35   document generated from a theory.  Each markup command takes a
    36   single @{syntax text} argument, which is passed as argument to a
    37   corresponding {\LaTeX} macro.  The default macros provided by
    38   @{file "~~/lib/texinputs/isabelle.sty"} can be redefined according
    39   to the needs of the underlying document and {\LaTeX} styles.
    40 
    41   Note that formal comments (\secref{sec:comments}) are similar to
    42   markup commands, but have a different status within Isabelle/Isar
    43   syntax.
    44 
    45   @{rail \<open>
    46     (@@{command chapter} | @@{command section} | @@{command subsection} |
    47       @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
    48     ;
    49     @@{command text_raw} @{syntax text}
    50   \<close>}
    51 
    52   \begin{description}
    53 
    54   \item @{command chapter}, @{command section}, @{command subsection}, and
    55   @{command subsubsection} mark chapter and section headings within the
    56   theory source; this works in any context, even before the initial
    57   @{command theory} command. The corresponding {\LaTeX} macros are
    58   @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
    59   @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
    60 
    61   \item @{command text} and @{command txt} specify paragraphs of plain text.
    62   This corresponds to a {\LaTeX} environment @{verbatim
    63   \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>}
    64   etc.
    65 
    66   \item @{command text_raw} inserts {\LaTeX} source directly into the
    67   output, without additional markup. Thus the full range of document
    68   manipulations becomes available, at the risk of messing up document
    69   output.
    70 
    71   \end{description}
    72 
    73   Except for @{command "text_raw"}, the text passed to any of the above
    74   markup commands may refer to formal entities via \emph{document
    75   antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
    76   present theory or proof context.
    77 
    78   \medskip The proof markup commands closely resemble those for theory
    79   specifications, but have a different formal status and produce
    80   different {\LaTeX} macros.
    81 \<close>
    82 
    83 
    84 section \<open>Document Antiquotations \label{sec:antiq}\<close>
    85 
    86 text \<open>
    87   \begin{matharray}{rcl}
    88     @{antiquotation_def "theory"} & : & @{text antiquotation} \\
    89     @{antiquotation_def "thm"} & : & @{text antiquotation} \\
    90     @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
    91     @{antiquotation_def "prop"} & : & @{text antiquotation} \\
    92     @{antiquotation_def "term"} & : & @{text antiquotation} \\
    93     @{antiquotation_def term_type} & : & @{text antiquotation} \\
    94     @{antiquotation_def typeof} & : & @{text antiquotation} \\
    95     @{antiquotation_def const} & : & @{text antiquotation} \\
    96     @{antiquotation_def abbrev} & : & @{text antiquotation} \\
    97     @{antiquotation_def typ} & : & @{text antiquotation} \\
    98     @{antiquotation_def type} & : & @{text antiquotation} \\
    99     @{antiquotation_def class} & : & @{text antiquotation} \\
   100     @{antiquotation_def "text"} & : & @{text antiquotation} \\
   101     @{antiquotation_def goals} & : & @{text antiquotation} \\
   102     @{antiquotation_def subgoals} & : & @{text antiquotation} \\
   103     @{antiquotation_def prf} & : & @{text antiquotation} \\
   104     @{antiquotation_def full_prf} & : & @{text antiquotation} \\
   105     @{antiquotation_def ML} & : & @{text antiquotation} \\
   106     @{antiquotation_def ML_op} & : & @{text antiquotation} \\
   107     @{antiquotation_def ML_type} & : & @{text antiquotation} \\
   108     @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
   109     @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
   110     @{antiquotation_def verbatim} & : & @{text antiquotation} \\
   111     @{antiquotation_def "file"} & : & @{text antiquotation} \\
   112     @{antiquotation_def "url"} & : & @{text antiquotation} \\
   113     @{antiquotation_def "cite"} & : & @{text antiquotation} \\
   114   \end{matharray}
   115 
   116   The overall content of an Isabelle/Isar theory may alternate between
   117   formal and informal text.  The main body consists of formal
   118   specification and proof commands, interspersed with markup commands
   119   (\secref{sec:markup}) or document comments (\secref{sec:comments}).
   120   The argument of markup commands quotes informal text to be printed
   121   in the resulting document, but may again refer to formal entities
   122   via \emph{document antiquotations}.
   123 
   124   For example, embedding @{verbatim \<open>@{term [show_types] "f x = a + x"}\<close>}
   125   within a text block makes
   126   \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.
   127 
   128   Antiquotations usually spare the author tedious typing of logical
   129   entities in full detail.  Even more importantly, some degree of
   130   consistency-checking between the main body of formal text and its
   131   informal explanation is achieved, since terms and types appearing in
   132   antiquotations are checked within the current theory or proof
   133   context.
   134 
   135   %% FIXME less monolithic presentation, move to individual sections!?
   136   @{rail \<open>
   137     '@{' antiquotation '}'
   138     ;
   139     @{syntax_def antiquotation}:
   140       @@{antiquotation theory} options @{syntax name} |
   141       @@{antiquotation thm} options styles @{syntax thmrefs} |
   142       @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
   143       @@{antiquotation prop} options styles @{syntax prop} |
   144       @@{antiquotation term} options styles @{syntax term} |
   145       @@{antiquotation (HOL) value} options styles @{syntax term} |
   146       @@{antiquotation term_type} options styles @{syntax term} |
   147       @@{antiquotation typeof} options styles @{syntax term} |
   148       @@{antiquotation const} options @{syntax term} |
   149       @@{antiquotation abbrev} options @{syntax term} |
   150       @@{antiquotation typ} options @{syntax type} |
   151       @@{antiquotation type} options @{syntax name} |
   152       @@{antiquotation class} options @{syntax name} |
   153       @@{antiquotation text} options @{syntax text}
   154     ;
   155     @{syntax antiquotation}:
   156       @@{antiquotation goals} options |
   157       @@{antiquotation subgoals} options |
   158       @@{antiquotation prf} options @{syntax thmrefs} |
   159       @@{antiquotation full_prf} options @{syntax thmrefs} |
   160       @@{antiquotation ML} options @{syntax text} |
   161       @@{antiquotation ML_op} options @{syntax text} |
   162       @@{antiquotation ML_type} options @{syntax text} |
   163       @@{antiquotation ML_structure} options @{syntax text} |
   164       @@{antiquotation ML_functor} options @{syntax text} |
   165       @@{antiquotation verbatim} options @{syntax text} |
   166       @@{antiquotation "file"} options @{syntax name} |
   167       @@{antiquotation file_unchecked} options @{syntax name} |
   168       @@{antiquotation url} options @{syntax name} |
   169       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
   170     ;
   171     options: '[' (option * ',') ']'
   172     ;
   173     option: @{syntax name} | @{syntax name} '=' @{syntax name}
   174     ;
   175     styles: '(' (style + ',') ')'
   176     ;
   177     style: (@{syntax name} +)
   178   \<close>}
   179 
   180   Note that the syntax of antiquotations may \emph{not} include source
   181   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
   182   text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
   183 
   184   \begin{description}
   185   
   186   \item @{text "@{theory A}"} prints the name @{text "A"}, which is
   187   guaranteed to refer to a valid ancestor theory in the current
   188   context.
   189 
   190   \item @{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
   191   Full fact expressions are allowed here, including attributes
   192   (\secref{sec:syn-att}).
   193 
   194   \item @{text "@{prop \<phi>}"} prints a well-typed proposition @{text
   195   "\<phi>"}.
   196 
   197   \item @{text "@{lemma \<phi> by m}"} proves a well-typed proposition
   198   @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
   199 
   200   \item @{text "@{term t}"} prints a well-typed term @{text "t"}.
   201   
   202   \item @{text "@{value t}"} evaluates a term @{text "t"} and prints
   203   its result, see also @{command_ref (HOL) value}.
   204 
   205   \item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
   206   annotated with its type.
   207 
   208   \item @{text "@{typeof t}"} prints the type of a well-typed term
   209   @{text "t"}.
   210 
   211   \item @{text "@{const c}"} prints a logical or syntactic constant
   212   @{text "c"}.
   213   
   214   \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
   215   @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
   216 
   217   \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
   218 
   219   \item @{text "@{type \<kappa>}"} prints a (logical or syntactic) type
   220     constructor @{text "\<kappa>"}.
   221 
   222   \item @{text "@{class c}"} prints a class @{text c}.
   223 
   224   \item @{text "@{text s}"} prints uninterpreted source text @{text
   225   s}.  This is particularly useful to print portions of text according
   226   to the Isabelle document style, without demanding well-formedness,
   227   e.g.\ small pieces of terms that should not be parsed or
   228   type-checked yet.
   229 
   230   \item @{text "@{goals}"} prints the current \emph{dynamic} goal
   231   state.  This is mainly for support of tactic-emulation scripts
   232   within Isar.  Presentation of goal states does not conform to the
   233   idea of human-readable proof documents!
   234 
   235   When explaining proofs in detail it is usually better to spell out
   236   the reasoning via proper Isar proof commands, instead of peeking at
   237   the internal machine configuration.
   238   
   239   \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but
   240   does not print the main goal.
   241   
   242   \item @{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"} prints the (compact) proof terms
   243   corresponding to the theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that this
   244   requires proof terms to be switched on for the current logic
   245   session.
   246   
   247   \item @{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \<dots>
   248   a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays
   249   information omitted in the compact proof term, which is denoted by
   250   ``@{text _}'' placeholders there.
   251   
   252   \item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type
   253   s}"}, @{text "@{ML_structure s}"}, and @{text "@{ML_functor s}"}
   254   check text @{text s} as ML value, infix operator, type, structure,
   255   and functor respectively.  The source is printed verbatim.
   256 
   257   \item @{text "@{verbatim s}"} prints uninterpreted source text literally
   258   as ASCII characters, using some type-writer font style.
   259 
   260   \item @{text "@{file path}"} checks that @{text "path"} refers to a
   261   file (or directory) and prints it verbatim.
   262 
   263   \item @{text "@{file_unchecked path}"} is like @{text "@{file
   264   path}"}, but does not check the existence of the @{text "path"}
   265   within the file-system.
   266 
   267   \item @{text "@{url name}"} produces markup for the given URL, which
   268   results in an active hyperlink within the text.
   269 
   270   \item @{text "@{cite name}"} produces a citation @{verbatim
   271   \<open>\cite{name}\<close>} in {\LaTeX}, where the name refers to some Bib{\TeX}
   272   database entry.
   273 
   274   The variant @{text "@{cite \<open>opt\<close> name}"} produces @{verbatim
   275   \<open>\cite[opt]{name}\<close>} with some free-form optional argument. Multiple names
   276   are output with commas, e.g. @{text "@{cite foo \<AND> bar}"} becomes
   277   @{verbatim \<open>\cite{foo,bar}\<close>}.
   278 
   279   The {\LaTeX} macro name is determined by the antiquotation option
   280   @{antiquotation_option_def cite_macro}, or the configuration option
   281   @{attribute cite_macro} in the context. For example, @{text "@{cite
   282   [cite_macro = nocite] foobar}"} produces @{verbatim \<open>\nocite{foobar}\<close>}.
   283 
   284   \end{description}
   285 \<close>
   286 
   287 
   288 subsection \<open>Styled antiquotations\<close>
   289 
   290 text \<open>The antiquotations @{text thm}, @{text prop} and @{text
   291   term} admit an extra \emph{style} specification to modify the
   292   printed result.  A style is specified by a name with a possibly
   293   empty number of arguments;  multiple styles can be sequenced with
   294   commas.  The following standard styles are available:
   295 
   296   \begin{description}
   297   
   298   \item @{text lhs} extracts the first argument of any application
   299   form with at least two arguments --- typically meta-level or
   300   object-level equality, or any other binary relation.
   301   
   302   \item @{text rhs} is like @{text lhs}, but extracts the second
   303   argument.
   304   
   305   \item @{text "concl"} extracts the conclusion @{text C} from a rule
   306   in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
   307   
   308   \item @{text "prem"} @{text n} extract premise number
   309   @{text "n"} from from a rule in Horn-clause
   310   normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
   311 
   312   \end{description}
   313 \<close>
   314 
   315 
   316 subsection \<open>General options\<close>
   317 
   318 text \<open>The following options are available to tune the printed output
   319   of antiquotations.  Note that many of these coincide with system and
   320   configuration options of the same names.
   321 
   322   \begin{description}
   323 
   324   \item @{antiquotation_option_def show_types}~@{text "= bool"} and
   325   @{antiquotation_option_def show_sorts}~@{text "= bool"} control
   326   printing of explicit type and sort constraints.
   327 
   328   \item @{antiquotation_option_def show_structs}~@{text "= bool"}
   329   controls printing of implicit structures.
   330 
   331   \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
   332   controls folding of abbreviations.
   333 
   334   \item @{antiquotation_option_def names_long}~@{text "= bool"} forces
   335   names of types and constants etc.\ to be printed in their fully
   336   qualified internal form.
   337 
   338   \item @{antiquotation_option_def names_short}~@{text "= bool"}
   339   forces names of types and constants etc.\ to be printed unqualified.
   340   Note that internalizing the output again in the current context may
   341   well yield a different result.
   342 
   343   \item @{antiquotation_option_def names_unique}~@{text "= bool"}
   344   determines whether the printed version of qualified names should be
   345   made sufficiently long to avoid overlap with names declared further
   346   back.  Set to @{text false} for more concise output.
   347 
   348   \item @{antiquotation_option_def eta_contract}~@{text "= bool"}
   349   prints terms in @{text \<eta>}-contracted form.
   350 
   351   \item @{antiquotation_option_def display}~@{text "= bool"} indicates
   352   if the text is to be output as multi-line ``display material'',
   353   rather than a small piece of text without line breaks (which is the
   354   default).
   355 
   356   In this mode the embedded entities are printed in the same style as
   357   the main theory text.
   358 
   359   \item @{antiquotation_option_def break}~@{text "= bool"} controls
   360   line breaks in non-display material.
   361 
   362   \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates
   363   if the output should be enclosed in double quotes.
   364 
   365   \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text
   366   name} to the print mode to be used for presentation.  Note that the
   367   standard setup for {\LaTeX} output is already present by default,
   368   including the modes @{text latex} and @{text xsymbols}.
   369 
   370   \item @{antiquotation_option_def margin}~@{text "= nat"} and
   371   @{antiquotation_option_def indent}~@{text "= nat"} change the margin
   372   or indentation for pretty printing of display material.
   373 
   374   \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
   375   determines the maximum number of subgoals to be printed (for goal-based
   376   antiquotation).
   377 
   378   \item @{antiquotation_option_def source}~@{text "= bool"} prints the
   379   original source text of the antiquotation arguments, rather than its
   380   internal representation.  Note that formal checking of
   381   @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
   382   enabled; use the @{antiquotation "text"} antiquotation for unchecked
   383   output.
   384 
   385   Regular @{text "term"} and @{text "typ"} antiquotations with @{text
   386   "source = false"} involve a full round-trip from the original source
   387   to an internalized logical entity back to a source form, according
   388   to the syntax of the current context.  Thus the printed output is
   389   not under direct control of the author, it may even fluctuate a bit
   390   as the underlying theory is changed later on.
   391 
   392   In contrast, @{antiquotation_option source}~@{text "= true"}
   393   admits direct printing of the given source text, with the desirable
   394   well-formedness check in the background, but without modification of
   395   the printed text.
   396 
   397   \end{description}
   398 
   399   For Boolean flags, ``@{text "name = true"}'' may be abbreviated as
   400   ``@{text name}''.  All of the above flags are disabled by default,
   401   unless changed specifically for a logic session in the corresponding
   402   @{verbatim "ROOT"} file.\<close>
   403 
   404 
   405 section \<open>Markup via command tags \label{sec:tags}\<close>
   406 
   407 text \<open>Each Isabelle/Isar command may be decorated by additional
   408   presentation tags, to indicate some modification in the way it is
   409   printed in the document.
   410 
   411   @{rail \<open>
   412     @{syntax_def tags}: ( tag * )
   413     ;
   414     tag: '%' (@{syntax ident} | @{syntax string})
   415   \<close>}
   416 
   417   Some tags are pre-declared for certain classes of commands, serving
   418   as default markup if no tags are given in the text:
   419 
   420   \medskip
   421   \begin{tabular}{ll}
   422     @{text "theory"} & theory begin/end \\
   423     @{text "proof"} & all proof commands \\
   424     @{text "ML"} & all commands involving ML code \\
   425   \end{tabular}
   426 
   427   \medskip The Isabelle document preparation system
   428   @{cite "isabelle-sys"} allows tagged command regions to be presented
   429   specifically, e.g.\ to fold proof texts, or drop parts of the text
   430   completely.
   431 
   432   For example ``@{command "by"}~@{text "%invisible auto"}'' causes
   433   that piece of proof to be treated as @{text invisible} instead of
   434   @{text "proof"} (the default), which may be shown or hidden
   435   depending on the document setup.  In contrast, ``@{command
   436   "by"}~@{text "%visible auto"}'' forces this text to be shown
   437   invariably.
   438 
   439   Explicit tag specifications within a proof apply to all subsequent
   440   commands of the same level of nesting.  For example, ``@{command
   441   "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' forces the whole
   442   sub-proof to be typeset as @{text visible} (unless some of its parts
   443   are tagged differently).
   444 
   445   \medskip Command tags merely produce certain markup environments for
   446   type-setting.  The meaning of these is determined by {\LaTeX}
   447   macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or
   448   by the document author.  The Isabelle document preparation tools
   449   also provide some high-level options to specify the meaning of
   450   arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
   451   parts of the text.  Logic sessions may also specify ``document
   452   versions'', where given tags are interpreted in some particular way.
   453   Again see @{cite "isabelle-sys"} for further details.
   454 \<close>
   455 
   456 
   457 section \<open>Railroad diagrams\<close>
   458 
   459 text \<open>
   460   \begin{matharray}{rcl}
   461     @{antiquotation_def "rail"} & : & @{text antiquotation} \\
   462   \end{matharray}
   463 
   464   @{rail \<open>
   465     'rail' (@{syntax string} | @{syntax cartouche})
   466   \<close>}
   467 
   468   The @{antiquotation rail} antiquotation allows to include syntax
   469   diagrams into Isabelle documents.  {\LaTeX} requires the style file
   470   @{file "~~/lib/texinputs/railsetup.sty"}, which can be used via
   471   @{verbatim \<open>\usepackage{railsetup}\<close>} in @{verbatim "root.tex"}, for
   472   example.
   473 
   474   The rail specification language is quoted here as Isabelle @{syntax
   475   string} or text @{syntax "cartouche"}; it has its own grammar given
   476   below.
   477 
   478   \begingroup
   479   \def\isasymnewline{\isatext{\tt\isacharbackslash<newline>}}
   480   @{rail \<open>
   481   rule? + ';'
   482   ;
   483   rule: ((identifier | @{syntax antiquotation}) ':')? body
   484   ;
   485   body: concatenation + '|'
   486   ;
   487   concatenation: ((atom '?'?) +) (('*' | '+') atom?)?
   488   ;
   489   atom: '(' body? ')' | identifier |
   490     '@'? (string | @{syntax antiquotation}) |
   491     '\<newline>'
   492   \<close>}
   493   \endgroup
   494 
   495   The lexical syntax of @{text "identifier"} coincides with that of
   496   @{syntax ident} in regular Isabelle syntax, but @{text string} uses
   497   single quotes instead of double quotes of the standard @{syntax
   498   string} category.
   499 
   500   Each @{text rule} defines a formal language (with optional name),
   501   using a notation that is similar to EBNF or regular expressions with
   502   recursion.  The meaning and visual appearance of these rail language
   503   elements is illustrated by the following representative examples.
   504 
   505   \begin{itemize}
   506 
   507   \item Empty @{verbatim "()"}
   508 
   509   @{rail \<open>()\<close>}
   510 
   511   \item Nonterminal @{verbatim "A"}
   512 
   513   @{rail \<open>A\<close>}
   514 
   515   \item Nonterminal via Isabelle antiquotation
   516   @{verbatim "@{syntax method}"}
   517 
   518   @{rail \<open>@{syntax method}\<close>}
   519 
   520   \item Terminal @{verbatim "'xyz'"}
   521 
   522   @{rail \<open>'xyz'\<close>}
   523 
   524   \item Terminal in keyword style @{verbatim "@'xyz'"}
   525 
   526   @{rail \<open>@'xyz'\<close>}
   527 
   528   \item Terminal via Isabelle antiquotation
   529   @{verbatim "@@{method rule}"}
   530 
   531   @{rail \<open>@@{method rule}\<close>}
   532 
   533   \item Concatenation @{verbatim "A B C"}
   534 
   535   @{rail \<open>A B C\<close>}
   536 
   537   \item Newline inside concatenation
   538   @{verbatim "A B C \<newline> D E F"}
   539 
   540   @{rail \<open>A B C \<newline> D E F\<close>}
   541 
   542   \item Variants @{verbatim "A | B | C"}
   543 
   544   @{rail \<open>A | B | C\<close>}
   545 
   546   \item Option @{verbatim "A ?"}
   547 
   548   @{rail \<open>A ?\<close>}
   549 
   550   \item Repetition @{verbatim "A *"}
   551 
   552   @{rail \<open>A *\<close>}
   553 
   554   \item Repetition with separator @{verbatim "A * sep"}
   555 
   556   @{rail \<open>A * sep\<close>}
   557 
   558   \item Strict repetition @{verbatim "A +"}
   559 
   560   @{rail \<open>A +\<close>}
   561 
   562   \item Strict repetition with separator @{verbatim "A + sep"}
   563 
   564   @{rail \<open>A + sep\<close>}
   565 
   566   \end{itemize}
   567 \<close>
   568 
   569 
   570 section \<open>Draft presentation\<close>
   571 
   572 text \<open>
   573   \begin{matharray}{rcl}
   574     @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   575   \end{matharray}
   576 
   577   @{rail \<open>
   578     @@{command display_drafts} (@{syntax name} +)
   579   \<close>}
   580 
   581   \begin{description}
   582 
   583   \item @{command "display_drafts"}~@{text paths} performs simple output of a
   584   given list of raw source files. Only those symbols that do not require
   585   additional {\LaTeX} packages are displayed properly, everything else is left
   586   verbatim.
   587 
   588   \end{description}
   589 \<close>
   590 
   591 end