5 chapter {* Comments for Authors of the Cookbook *} |
5 chapter {* Comments for Authors of the Cookbook *} |
6 |
6 |
7 text {* |
7 text {* |
8 |
8 |
9 \begin{itemize} |
9 \begin{itemize} |
10 \item You can make references to other Isabelle manuals using the |
10 \item You can include references to other Isabelle manuals using the |
11 reference names from those manuals. To do this the following |
11 reference names from those manuals. To do this the following |
12 four latex commands are defined: |
12 four latex commands are defined: |
13 |
13 |
14 \begin{center} |
14 \begin{center} |
15 \begin{tabular}{l|c|c} |
15 \begin{tabular}{l|c|c} |
23 in the implementation manual, namely \ichcite{ch:logic}. |
23 in the implementation manual, namely \ichcite{ch:logic}. |
24 |
24 |
25 \item There are various document antiquotations defined for the |
25 \item There are various document antiquotations defined for the |
26 cookbook so that written text can be kept in sync with the |
26 cookbook so that written text can be kept in sync with the |
27 Isabelle code and also that responses of the ML-compiler can be shown. |
27 Isabelle code and also that responses of the ML-compiler can be shown. |
28 For example |
28 The are: |
29 |
29 |
30 \begin{itemize} |
30 \begin{itemize} |
31 \item[$\bullet$] @{text "@{ML \"\<dots>\"}"} |
31 \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value computations. It checks whether |
32 \item[$\bullet$] @{text "@{ML_open \"\<dots>\"}"} |
32 the ML-expression is valid ML-code, but only works for closed expression. |
33 \item[$\bullet$] @{text "@{ML_response \"\<dots>\"}"} |
33 \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text ML}-antiquotation except, |
34 \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\"}"} |
34 that it can also deal with open expressions and expressions that need to be evaluated inside structures. |
35 \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} |
35 The free variables or structures need to be listed after the @{ML_text "for"}. For example |
|
36 @{text "@{ML_open \"a + b\" for a b}"}. |
|
37 \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} The first |
|
38 expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the |
|
39 second is a pattern that specifies the result the first expression |
|
40 produces. This specification can contain @{text [quotes] "\<dots>"} for parts that |
|
41 can be omitted. The actual response will be checked against the |
|
42 specification. For example @{text "@{ML_response \"(1+2,3)\" |
|
43 \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be |
|
44 constructed. It does not work when the code produces an exception or is an |
|
45 abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
|
46 |
|
47 \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like the |
|
48 @{ML_text ML_response}-anti\-quotation, except that the result-specification is not |
|
49 checked. |
|
50 \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when referring to a file. |
|
51 It checks whether the file exists. |
36 \end{itemize} |
52 \end{itemize} |
37 |
53 |
38 (FIXME: explain their usage) |
54 \item Functions and value bindings cannot be defined inside antiquotations; they need |
|
55 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
|
56 environments. Some \LaTeX-hack, however, does not print the environment markers. |
39 |
57 |
40 \end{itemize} |
58 \end{itemize} |
41 |
59 |
42 *} |
60 *} |
43 |
61 |
44 |
62 |
|
63 |
45 end |
64 end |