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