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