79 |
79 |
80 Note that formal comments (\secref{sec:comments}) are similar to |
80 Note that formal comments (\secref{sec:comments}) are similar to |
81 markup commands, but have a different status within Isabelle/Isar |
81 markup commands, but have a different status within Isabelle/Isar |
82 syntax. |
82 syntax. |
83 |
83 |
84 \begin{rail} |
84 @{rail " |
85 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text |
85 (@@{command chapter} | @@{command section} | @@{command subsection} | |
86 ; |
86 @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text} |
87 ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text |
87 ; |
88 ; |
88 (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} | |
89 \end{rail} |
89 @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text} |
|
90 "} |
90 |
91 |
91 \begin{description} |
92 \begin{description} |
92 |
93 |
93 \item @{command header} provides plain text markup just preceding |
94 \item @{command header} provides plain text markup just preceding |
94 the formal beginning of a theory. The corresponding {\LaTeX} macro |
95 the formal beginning of a theory. The corresponding {\LaTeX} macro |
176 consistency-checking between the main body of formal text and its |
177 consistency-checking between the main body of formal text and its |
177 informal explanation is achieved, since terms and types appearing in |
178 informal explanation is achieved, since terms and types appearing in |
178 antiquotations are checked within the current theory or proof |
179 antiquotations are checked within the current theory or proof |
179 context. |
180 context. |
180 |
181 |
181 \begin{rail} |
182 @{rail " |
182 atsign lbrace antiquotation rbrace |
183 '@{' antiquotation '}' |
183 ; |
184 ; |
184 |
185 @{syntax_def antiquotation}: |
185 antiquotation: |
186 @@{antiquotation theory} options @{syntax name} | |
186 'theory' options name | |
187 @@{antiquotation thm} options styles @{syntax thmrefs} | |
187 'thm' options styles thmrefs | |
188 @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} | |
188 'lemma' options prop 'by' method | |
189 @@{antiquotation prop} options styles @{syntax prop} | |
189 'prop' options styles prop | |
190 @@{antiquotation term} options styles @{syntax term} | |
190 'term' options styles term | |
191 @@{antiquotation term_type} options styles @{syntax term} | |
191 'term_type' options styles term | |
192 @@{antiquotation typeof} options styles @{syntax term} | |
192 'typeof' options styles term | |
193 @@{antiquotation const} options @{syntax term} | |
193 'const' options term | |
194 @@{antiquotation abbrev} options @{syntax term} | |
194 'abbrev' options term | |
195 @@{antiquotation typ} options @{syntax type} | |
195 'typ' options type | |
196 @@{antiquotation type} options @{syntax name} | |
196 'type' options name | |
197 @@{antiquotation class} options @{syntax name} | |
197 'class' options name | |
198 @@{antiquotation text} options @{syntax name} | |
198 'text' options name | |
199 @@{antiquotation goals} options | |
199 'goals' options | |
200 @@{antiquotation subgoals} options | |
200 'subgoals' options | |
201 @@{antiquotation prf} options @{syntax thmrefs} | |
201 'prf' options thmrefs | |
202 @@{antiquotation full_prf} options @{syntax thmrefs} | |
202 'full_prf' options thmrefs | |
203 @@{antiquotation ML} options @{syntax name} | |
203 'ML' options name | |
204 @@{antiquotation ML_type} options @{syntax name} | |
204 'ML_type' options name | |
205 @@{antiquotation ML_struct} options @{syntax name} | |
205 'ML_struct' options name | |
206 @@{antiquotation \"file\"} options @{syntax name} |
206 'file' options name |
|
207 ; |
207 ; |
208 options: '[' (option * ',') ']' |
208 options: '[' (option * ',') ']' |
209 ; |
209 ; |
210 option: name | name '=' name |
210 option: @{syntax name} | @{syntax name} '=' @{syntax name} |
211 ; |
211 ; |
212 styles: '(' (style + ',') ')' |
212 styles: '(' (style + ',') ')' |
213 ; |
213 ; |
214 style: (name +) |
214 style: (@{syntax name} +) |
215 ; |
215 "} %% FIXME check lemma |
216 \end{rail} |
|
217 |
216 |
218 Note that the syntax of antiquotations may \emph{not} include source |
217 Note that the syntax of antiquotations may \emph{not} include source |
219 comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim |
218 comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim |
220 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim |
219 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim |
221 "*"}@{verbatim "}"}. |
220 "*"}@{verbatim "}"}. |
418 |
417 |
419 text {* Each Isabelle/Isar command may be decorated by additional |
418 text {* Each Isabelle/Isar command may be decorated by additional |
420 presentation tags, to indicate some modification in the way it is |
419 presentation tags, to indicate some modification in the way it is |
421 printed in the document. |
420 printed in the document. |
422 |
421 |
423 \indexouternonterm{tags} |
422 @{rail " |
424 \begin{rail} |
423 @{syntax_def tags}: ( tag * ) |
425 tags: ( tag * ) |
424 ; |
426 ; |
425 tag: '%' (@{syntax ident} | @{syntax string}) |
427 tag: '\%' (ident | string) |
426 "} |
428 \end{rail} |
|
429 |
427 |
430 Some tags are pre-declared for certain classes of commands, serving |
428 Some tags are pre-declared for certain classes of commands, serving |
431 as default markup if no tags are given in the text: |
429 as default markup if no tags are given in the text: |
432 |
430 |
433 \medskip |
431 \medskip |
473 \begin{matharray}{rcl} |
471 \begin{matharray}{rcl} |
474 @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
472 @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
475 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
473 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
476 \end{matharray} |
474 \end{matharray} |
477 |
475 |
478 \begin{rail} |
476 @{rail " |
479 ('display_drafts' | 'print_drafts') (name +) |
477 (@@{command display_drafts} | @@{command print_drafts}) (@{syntax name} +) |
480 ; |
478 |
481 \end{rail} |
479 "} |
482 |
480 |
483 \begin{description} |
481 \begin{description} |
484 |
482 |
485 \item @{command "display_drafts"}~@{text paths} and @{command |
483 \item @{command "display_drafts"}~@{text paths} and @{command |
486 "print_drafts"}~@{text paths} perform simple output of a given list |
484 "print_drafts"}~@{text paths} perform simple output of a given list |