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