18 four \LaTeX{} commands are defined: |
18 four \LaTeX{} commands are defined: |
19 |
19 |
20 \begin{center} |
20 \begin{center} |
21 \begin{tabular}{l|c|c} |
21 \begin{tabular}{l|c|c} |
22 & Chapters & Sections\\\hline |
22 & Chapters & Sections\\\hline |
23 Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\ |
23 Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\ |
24 Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\ |
24 Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\ |
25 \end{tabular} |
25 \end{tabular} |
26 \end{center} |
26 \end{center} |
27 |
27 |
28 So @{ML_text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic |
28 So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic |
29 in the implementation manual, namely \ichcite{ch:logic}. |
29 in the implementation manual, namely \ichcite{ch:logic}. |
30 |
30 |
31 \item There are various document antiquotations defined for the |
31 \item There are various document antiquotations defined for the |
32 cookbook. They allow to check the written text against the current |
32 cookbook. They allow to check the written text against the current |
33 Isabelle code and also allow to show responses of the ML-compiler. |
33 Isabelle code and also allow to show responses of the ML-compiler. |
35 appropriate. |
35 appropriate. |
36 |
36 |
37 The following antiquotations are defined: |
37 The following antiquotations are defined: |
38 |
38 |
39 \begin{itemize} |
39 \begin{itemize} |
40 \item[$\bullet$] @{text "@{ML \"\<dots>\" for \<dots> in \<dots>}"} should be used for |
40 \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used |
41 displaying any ML-ex\-pression, because it checks whether the expression is valid |
41 for displaying any ML-ex\-pression, because the antiquotation checks whether |
42 ML-code. The @{text "for"} and @{text "in"} arguments are optional. The |
42 the expression is valid ML-code. The @{text "for"}- and @{text |
43 former is used for evaluating open expressions by giving a list of |
43 "in"}-arguments are optional. The former is used for evaluating open |
44 free variables. The latter is used to indicate in which structure or structures the |
44 expressions by giving a list of free variables. The latter is used to |
45 ML-expression should be evaluated. Examples are: |
45 indicate in which structure or structures the ML-expression should be |
|
46 evaluated. Examples are: |
46 |
47 |
47 \begin{center}\small |
48 \begin{center}\small |
48 \begin{tabular}{l} |
49 \begin{tabular}{lll} |
49 @{text "@{ML \"1 + 3\"}"}\\ |
50 @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\ |
50 @{text "@{ML \"a + b\" for a b}"}\\ |
51 @{text "@{ML \"a + b\" for a b}"} & produce & @{ML "a + b" for a b}\\ |
51 @{text "@{ML Ident in OuterLex}"} |
52 @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\ |
52 \end{tabular} |
53 \end{tabular} |
53 \end{center} |
54 \end{center} |
54 |
55 |
55 \item[$\bullet$] @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} should be used to |
56 \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to |
56 display ML-ex\-pressions and their response. |
57 display ML-expressions and their response. The first expression is checked |
57 The first expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the |
58 like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern |
58 second is a pattern that specifies the result the first expression |
59 that specifies the result the first expression produces. This pattern can |
59 produces. This specification can contain @{text "\<dots>"} for parts that |
60 contain @{text "\<dots>"} for parts that you like to omit. The response of the |
60 you like to omit. The response of the first expresion will be checked against |
61 first expression will be checked against this pattern. Examples are: |
61 this specification. An example is @{text "@{ML_response \"(1+2,3)\" |
62 |
62 \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be |
63 \begin{center}\small |
|
64 \begin{tabular}{l} |
|
65 @{text "@{ML_response \"1+2\" \"3\"}"}\\ |
|
66 @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"} |
|
67 \end{tabular} |
|
68 \end{center} |
|
69 |
|
70 which produce respectively |
|
71 |
|
72 \begin{center}\small |
|
73 \begin{tabular}{p{3cm}p{3cm}} |
|
74 @{ML_response "1+2" "3"} & |
|
75 @{ML_response "(1+2,3)" "(3,\<dots>)"} |
|
76 \end{tabular} |
|
77 \end{center} |
|
78 |
|
79 Note that 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 |
80 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}). |
81 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
65 |
82 |
66 \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like |
83 \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just |
67 the @{ML_text ML_response}-anti\-quotation, except that the |
84 like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above, |
68 result-specification is not checked. Use this antiquotation |
85 except that the result-specification is not checked. Use this antiquotation |
69 if the result cannot be constructed or the code generates an exception. |
86 when the result cannot be constructed or the code generates an |
|
87 exception. Examples are: |
|
88 |
|
89 \begin{center}\small |
|
90 \begin{tabular}{ll} |
|
91 @{text "@{ML_response"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\ |
|
92 & @{text "\"a + b = c\"}"}\smallskip\\ |
|
93 @{text "@{ML_response"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ |
|
94 & @{text "\"Exception FAIL raised\"}"} |
|
95 \end{tabular} |
|
96 \end{center} |
|
97 |
70 |
98 |
71 \item[$\bullet$] @{text "@{ML_response_fake_both \"\<dots>\" \"\<dots>\"}"} can be |
99 \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be |
72 used to show erroneous code. Neither the code nor the response will be |
100 used to show erroneous code. Neither the code nor the response will be |
73 chacked. |
101 checked. An example is: |
74 |
102 |
75 \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when |
103 \begin{center}\small |
|
104 \begin{tabular}{ll} |
|
105 @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\ |
|
106 & @{text "\"Type unification failed \<dots>\"}"} |
|
107 \end{tabular} |
|
108 \end{center} |
|
109 |
|
110 \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when |
76 referring to a file. It checks whether the file exists. |
111 referring to a file. It checks whether the file exists. |
77 \end{itemize} |
112 \end{itemize} |
|
113 |
|
114 The listed antiquotations honour options including @{text "[display]"} and |
|
115 @{text "[quotes]"}. For example |
|
116 |
|
117 \begin{center}\small |
|
118 @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"} |
|
119 \end{center} |
|
120 |
|
121 while |
|
122 |
|
123 \begin{center}\small |
|
124 @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"} |
|
125 \end{center} |
|
126 |
78 |
127 |
79 |
128 |
80 \item Functions and value bindings cannot be defined inside antiquotations; they need |
129 \item Functions and value bindings cannot be defined inside antiquotations; they need |
81 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
130 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
82 environments. In this way they are also checked by the compiler. Some \LaTeX-hack, however, |
131 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
83 ensures that the environment markers are not printed. |
132 the Cookbook, however, ensures that the environment markers are not printed. |
84 |
133 |
85 \item Line numbers can be printed using |
134 \item Line numbers can be printed using |
86 \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
135 \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
87 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
136 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
88 |
137 |