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