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