37 appropriate. |
37 appropriate. |
38 |
38 |
39 The following antiquotations are defined: |
39 The following antiquotations are defined: |
40 |
40 |
41 \begin{itemize} |
41 \begin{itemize} |
42 \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> should be used |
42 \item[$\bullet$] \<open>@{ML \<open>expr\<close> for vars in structs}\<close> should be used |
43 for displaying any ML-ex\-pression, because the antiquotation checks whether |
43 for displaying any ML-ex\-pression, because the antiquotation checks whether |
44 the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open |
44 the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open |
45 expressions by giving a list of free variables. The latter is used to |
45 expressions by giving a list of free variables. The latter is used to |
46 indicate in which structure or structures the ML-expression should be |
46 indicate in which structure or structures the ML-expression should be |
47 evaluated. Examples are: |
47 evaluated. Examples are: |
48 |
48 |
49 \begin{center}\small |
49 \begin{center}\small |
50 \begin{tabular}{lll} |
50 \begin{tabular}{lll} |
51 \<open>@{ML "1 + 3"}\<close> & & @{ML "1 + 3"}\\ |
51 \<open>@{ML \<open>1 + 3\<close>}\<close> & & @{ML \<open>1 + 3\<close>}\\ |
52 \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\ |
52 \<open>@{ML \<open>a + b\<close> for a b}\<close> & \;\;produce\;\; & @{ML \<open>a + b\<close> for a b}\\ |
53 \<open>@{ML Ident in OuterLex}\<close> & & @{ML Ident in OuterLex}\\ |
53 \<open>@{ML explode in Symbol}\<close> & & @{ML explode in Symbol}\\ |
54 \end{tabular} |
54 \end{tabular} |
55 \end{center} |
55 \end{center} |
56 |
56 |
57 \item[$\bullet$] \<open>@{ML_matchresult "expr" "pat"}\<close> should be used to |
57 \item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> should be used to |
58 display ML-expressions and their response. The first expression is checked |
58 display ML-expressions and their response. The first expression is checked |
59 like in the antiquotation \<open>@{ML "expr"}\<close>; the second is a pattern |
59 like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern |
60 that specifies the result the first expression produces. This pattern can |
60 that specifies the result the first expression produces. This pattern can |
61 contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the |
61 contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the |
62 first expression will be checked against this pattern. Examples are: |
62 first expression will be checked against this pattern. Examples are: |
63 |
63 |
64 \begin{center}\small |
64 \begin{center}\small |
65 \begin{tabular}{l} |
65 \begin{tabular}{l} |
66 \<open>@{ML_matchresult "1+2" "3"}\<close>\\ |
66 \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\ |
67 \<open>@{ML_matchresult "(1+2,3)" "(3,\<dots>)"}\<close> |
67 \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,\<dots>)\<close>}\<close> |
68 \end{tabular} |
68 \end{tabular} |
69 \end{center} |
69 \end{center} |
70 |
70 |
71 which produce respectively |
71 which produce respectively |
72 |
72 |
73 \begin{center}\small |
73 \begin{center}\small |
74 \begin{tabular}{p{3cm}p{3cm}} |
74 \begin{tabular}{p{3cm}p{3cm}} |
75 @{ML_matchresult "1+2" "3"} & |
75 @{ML_matchresult \<open>1+2\<close> \<open>3\<close>} & |
76 @{ML_matchresult "(1+2,3)" "(3,\<dots>)"} |
76 @{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>} |
77 \end{tabular} |
77 \end{tabular} |
78 \end{center} |
78 \end{center} |
79 |
79 |
80 Note that this antiquotation can only be used when the result can be |
80 Note that this antiquotation can only be used when the result can be |
81 constructed: it does not work when the code produces an exception or returns |
81 constructed: it does not work when the code produces an exception or returns |
82 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
82 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
83 |
83 |
84 \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just |
84 \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just |
85 like the antiquotation \<open>@{ML_matchresult "expr" "pat"}\<close> above, |
85 like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above, |
86 except that the result-specification is not checked. Use this antiquotation |
86 except that the result-specification is not checked. Use this antiquotation |
87 when the result cannot be constructed or the code generates an |
87 when the result cannot be constructed or the code generates an |
88 exception. Examples are: |
88 exception. Examples are: |
89 |
89 |
90 \begin{center}\small |
90 \begin{center}\small |
91 \begin{tabular}{ll} |
91 \begin{tabular}{ll} |
92 \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\ |
92 \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term "a + b = c"}"}\<close>\\ |
93 & \<open>"a + b = c"}\<close>\smallskip\\ |
93 & \<open>"a + b = c"}\<close>\smallskip\\ |
94 \<open>@{ML_matchresult_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ |
94 \<open>@{ML_matchresult_fake\<close> & \<open>"($$ "x") (explode "world")"\<close>\\ |
95 & \<open>"Exception FAIL raised"}\<close> |
95 & \<open>"Exception FAIL raised"}\<close> |
96 \end{tabular} |
96 \end{tabular} |
97 \end{center} |
97 \end{center} |
98 |
98 |
99 which produce respectively |
99 which produce respectively |
100 |
100 |
101 \begin{center}\small |
101 \begin{center}\small |
102 \begin{tabular}{p{7.2cm}} |
102 \begin{tabular}{p{7.2cm}} |
103 @{ML_matchresult_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\ |
103 @{ML_matchresult_fake \<open>Thm.cterm_of @{context} @{term "a + b = c"}\<close> \<open>a + b = c\<close>}\smallskip\\ |
104 @{ML_matchresult_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"} |
104 @{ML_matchresult_fake \<open>($$ "x") (Symbol.explode "world")\<close> \<open>Exception FAIL raised\<close>} |
105 \end{tabular} |
105 \end{tabular} |
106 \end{center} |
106 \end{center} |
107 |
107 |
108 This output mimics to some extend what the user sees when running the |
108 This output mimics to some extend what the user sees when running the |
109 code. |
109 code. |
112 used to show erroneous code. Neither the code nor the response will be |
112 used to show erroneous code. Neither the code nor the response will be |
113 checked. An example is: |
113 checked. An example is: |
114 |
114 |
115 \begin{center}\small |
115 \begin{center}\small |
116 \begin{tabular}{ll} |
116 \begin{tabular}{ll} |
117 \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\ |
117 \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\ |
118 & \<open>"Type unification failed \<dots>"}\<close> |
118 & \<open>"Type unification failed \<dots>"}\<close> |
119 \end{tabular} |
119 \end{tabular} |
120 \end{center} |
120 \end{center} |
121 |
121 |
122 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
122 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
123 referring to a file. It checks whether the file exists. An example |
123 referring to a file. It checks whether the file exists. An example |
124 is |
124 is |
125 |
125 |
126 @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"} |
126 @{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>} |
127 \end{itemize} |
127 \end{itemize} |
128 |
128 |
129 The listed antiquotations honour options including \<open>[display]\<close> and |
129 The listed antiquotations honour options including \<open>[display]\<close> and |
130 \<open>[quotes]\<close>. For example |
130 \<open>[quotes]\<close>. For example |
131 |
131 |
132 \begin{center}\small |
132 \begin{center}\small |
133 \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"} |
133 \<open>@{ML [quotes] \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces\;\; @{text [quotes] "foobar"} |
134 \end{center} |
134 \end{center} |
135 |
135 |
136 whereas |
136 whereas |
137 |
137 |
138 \begin{center}\small |
138 \begin{center}\small |
139 \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close> |
139 \<open>@{ML \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces only\;\; \<open>foobar\<close> |
140 \end{center} |
140 \end{center} |
141 |
141 |
142 \item Functions and value bindings cannot be defined inside antiquotations; they need |
142 \item Functions and value bindings cannot be defined inside antiquotations; they need |
143 to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> |
143 to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> |
144 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
144 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |