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