17 Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\ |
23 Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\ |
18 Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\ |
24 Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\ |
19 \end{tabular} |
25 \end{tabular} |
20 \end{center} |
26 \end{center} |
21 |
27 |
22 So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic |
28 So @{ML_text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic |
23 in the implementation manual, namely \ichcite{ch:logic}. |
29 in the implementation manual, namely \ichcite{ch:logic}. |
24 |
30 |
25 \item There are various document antiquotations defined for the |
31 \item There are various document antiquotations defined for the |
26 cookbook. This allows to check the written text against the current |
32 cookbook. They allow to check the written text against the current |
27 Isabelle code and also that responses of the ML-compiler can be shown. |
33 Isabelle code and also allow to show responses of the ML-compiler. |
28 Therefore authors are strongly encouraged to use antiquotations wherever |
34 Therefore authors are strongly encouraged to use antiquotations wherever |
29 it is appropriate. |
35 appropriate. |
30 |
36 |
31 The following antiquotations are in use: |
37 The following antiquotations are defined: |
32 |
38 |
33 \begin{itemize} |
39 \begin{itemize} |
34 \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value |
40 \item[$\bullet$] @{text "@{ML \"\<dots>\" for \<dots> in \<dots>}"} should be used for |
35 computations. It checks whether the ML-expression is valid ML-code, but only |
41 displaying any ML-ex\-pression, because it checks whether the expression is valid |
36 works for closed expression. |
42 ML-code. The @{text "for"} and @{text "in"} arguments are optional. The |
|
43 former is used for evaluating open expressions by giving a list of |
|
44 free variables. The latter is used to indicate in which structure or structures the |
|
45 ML-expression should be evaluated. Examples are: |
|
46 |
|
47 \begin{center} |
|
48 \begin{tabular}{l} |
|
49 @{text "@{ML \"1 + 3\"}"}\\ |
|
50 @{text "@{ML \"a + b\" for a b}"}\\ |
|
51 @{text "@{ML Ident in OuterLex}"} |
|
52 \end{tabular} |
|
53 \end{center} |
37 |
54 |
38 \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text |
55 \item[$\bullet$] @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} should be used to |
39 ML}-antiquotation except, that it can also deal with open expressions and |
56 display ML-ex\-pressions and their response. |
40 expressions that need to be evaluated inside structures. The free variables |
57 The first expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the |
41 or structures need to be listed after the @{ML_text "for"}. For example |
58 second is a pattern that specifies the result the first expression |
42 @{text "@{ML_open \"a + b\" for a b}"}. |
59 produces. This specification can contain @{text "\<dots>"} for parts that |
|
60 you like to omit. The response of the first expresion will be checked against |
|
61 this specification. An example is @{text "@{ML_response \"(1+2,3)\" |
|
62 \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be |
|
63 constructed: it does not work when the code produces an exception or returns |
|
64 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
43 |
65 |
44 \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} The first |
66 \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like |
45 expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the |
67 the @{ML_text ML_response}-anti\-quotation, except that the |
46 second is a pattern that specifies the result the first expression |
68 result-specification is not checked. Use this antiquotation |
47 produces. This specification can contain @{text [quotes] "\<dots>"} for parts that |
69 if the result cannot be constructed or the code generates an exception. |
48 can be omitted. The actual response will be checked against the |
|
49 specification. For example @{text "@{ML_response \"(1+2,3)\" |
|
50 \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be |
|
51 constructed. It does not work when the code produces an exception or is an |
|
52 abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
|
53 |
70 |
54 \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like |
71 \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when |
55 the @{ML_text ML_response}-anti\-quotation, except that the |
|
56 result-specification is not checked. |
|
57 |
|
58 \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when |
|
59 referring to a file. It checks whether the file exists. |
72 referring to a file. It checks whether the file exists. |
60 \end{itemize} |
73 \end{itemize} |
61 |
74 |
62 |
75 |
63 \item Functions and value bindings cannot be defined inside antiquotations; they need |
76 \item Functions and value bindings cannot be defined inside antiquotations; they need |
64 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
77 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
65 environments. Some \LaTeX-hack, however, does not print the environment markers. |
78 environments. In this way they are also checked by the compiler. Some \LaTeX-hack, however, |
|
79 ensures that the environment markers are not printed. |
66 |
80 |
67 \item Line numbers for code can be shown using |
81 \item Line numbers can be printed using |
68 \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}. |
82 \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
|
83 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
69 |
84 |
70 \end{itemize} |
85 \end{itemize} |
71 |
86 |
72 *} |
87 *} |
73 |
88 |