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