21 |
21 |
22 So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic |
22 So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic |
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. This allows to check the written text against the current |
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 The are: |
28 Therefore authors are strongly encouraged to use antiquotations wherever |
|
29 it is appropriate. |
|
30 |
|
31 The following antiquotations are in use: |
29 |
32 |
30 \begin{itemize} |
33 \begin{itemize} |
31 \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value computations. It checks whether |
34 \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value |
32 the ML-expression is valid ML-code, but only works for closed expression. |
35 computations. It checks whether the ML-expression is valid ML-code, but only |
33 \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text ML}-antiquotation except, |
36 works for closed expression. |
34 that it can also deal with open expressions and expressions that need to be evaluated inside structures. |
37 |
35 The free variables or structures need to be listed after the @{ML_text "for"}. For example |
38 \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text |
|
39 ML}-antiquotation except, that it can also deal with open expressions and |
|
40 expressions that need to be evaluated inside structures. The free variables |
|
41 or structures need to be listed after the @{ML_text "for"}. For example |
36 @{text "@{ML_open \"a + b\" for a b}"}. |
42 @{text "@{ML_open \"a + b\" for a b}"}. |
|
43 |
37 \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} The first |
44 \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} The first |
38 expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the |
45 expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the |
39 second is a pattern that specifies the result the first expression |
46 second is a pattern that specifies the result the first expression |
40 produces. This specification can contain @{text [quotes] "\<dots>"} for parts that |
47 produces. This specification can contain @{text [quotes] "\<dots>"} for parts that |
41 can be omitted. The actual response will be checked against the |
48 can be omitted. The actual response will be checked against the |
42 specification. For example @{text "@{ML_response \"(1+2,3)\" |
49 specification. For example @{text "@{ML_response \"(1+2,3)\" |
43 \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be |
50 \"(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 |
51 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}). |
52 abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
46 |
53 |
47 \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like the |
54 \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like |
48 @{ML_text ML_response}-anti\-quotation, except that the result-specification is not |
55 the @{ML_text ML_response}-anti\-quotation, except that the |
49 checked. |
56 result-specification is not checked. |
50 \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when referring to a file. |
57 |
51 It checks whether the file exists. |
58 \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when |
|
59 referring to a file. It checks whether the file exists. |
52 \end{itemize} |
60 \end{itemize} |
|
61 |
53 |
62 |
54 \item Functions and value bindings cannot be defined inside antiquotations; they need |
63 \item Functions and value bindings cannot be defined inside antiquotations; they need |
55 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
64 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
56 environments. Some \LaTeX-hack, however, does not print the environment markers. |
65 environments. Some \LaTeX-hack, however, does not print the environment markers. |
|
66 |
|
67 \item Line numbers for code can be shown using |
|
68 \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}. |
57 |
69 |
58 \end{itemize} |
70 \end{itemize} |
59 |
71 |
60 *} |
72 *} |
61 |
73 |