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