56 |
56 |
57 \item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<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 \<open>expr\<close>}\<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] "_"} (which will be printed as @{text [quotes] "\<dots>"}) |
|
62 for parts that you like to omit. The response of the |
62 first expression will be checked against this pattern. Examples are: |
63 first expression will be checked against this pattern. Examples are: |
63 |
64 |
64 \begin{center}\small |
65 \begin{center}\small |
65 \begin{tabular}{l} |
66 \begin{tabular}{l} |
66 \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\ |
67 \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\ |
67 \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,\<dots>)\<close>}\<close> |
68 \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}\<close> |
68 \end{tabular} |
69 \end{tabular} |
69 \end{center} |
70 \end{center} |
70 |
71 |
71 which produce respectively |
72 which produce respectively |
72 |
73 |
79 |
80 |
80 Note that this antiquotation can only be used when the result can be |
81 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 |
82 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}). |
83 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
83 |
84 |
84 \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just |
85 \item[$\bullet$] \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> works just |
85 like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above, |
86 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 |
87 except that the result-specification is not checked. Use this antiquotation |
87 when the result cannot be constructed or the code generates an |
88 when the result cannot be constructed or the code generates an |
88 exception. Examples are: |
89 exception. Examples are: |
89 |
90 |
90 \begin{center}\small |
91 \begin{center}\small |
91 \begin{tabular}{ll} |
92 \begin{tabular}{ll} |
92 \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term "a + b = c"}"}\<close>\\ |
93 \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>}\<close>\\ |
93 & \<open>"a + b = c"}\<close>\smallskip\\ |
94 & \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ |
94 \<open>@{ML_matchresult_fake\<close> & \<open>"($$ "x") (explode "world")"\<close>\\ |
95 \<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ |
95 & \<open>"Exception FAIL raised"}\<close> |
96 & \<open>\<open>Exception FAIL raised\<close>}\<close> |
96 \end{tabular} |
97 \end{tabular} |
97 \end{center} |
98 \end{center} |
98 |
99 |
99 which produce respectively |
100 which produce respectively |
100 |
101 |
106 \end{center} |
107 \end{center} |
107 |
108 |
108 This output mimics to some extend what the user sees when running the |
109 This output mimics to some extend what the user sees when running the |
109 code. |
110 code. |
110 |
111 |
111 \item[$\bullet$] \<open>@{ML_matchresult_fake_both "expr" "pat"}\<close> can be |
112 \item[$\bullet$] \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close> can be |
112 used to show erroneous code. Neither the code nor the response will be |
113 used to show erroneous code. Neither the code nor the response will be |
113 checked. An example is: |
114 checked. An example is: |
114 |
115 |
115 \begin{center}\small |
116 \begin{center}\small |
116 \begin{tabular}{ll} |
117 \begin{tabular}{ll} |
117 \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\ |
118 \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\ |
118 & \<open>"Type unification failed \<dots>"}\<close> |
119 & \<open>"Type unification failed \<dots>"}\<close> |
119 \end{tabular} |
120 \end{tabular} |
120 \end{center} |
121 \end{center} |
121 |
122 |
|
123 \item[$\bullet$] \<open>@{ML_response \<open>expr\<close>}\<close> can be |
|
124 used to show the expression and the corresponding output. An example is: |
|
125 |
|
126 \begin{center}\small |
|
127 \begin{tabular}{ll} |
|
128 \<open>@{ML_response\<close> & \<open>\<open>1 upto 10\<close>}\<close> |
|
129 \end{tabular} |
|
130 \end{center} |
|
131 |
|
132 which produce respectively |
|
133 |
|
134 \begin{center}\small |
|
135 \begin{tabular}{p{3cm}p{3cm}} |
|
136 @{ML_response \<open>1 upto 10\<close>} |
|
137 \end{tabular} |
|
138 \end{center} |
|
139 |
|
140 |
122 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
141 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
123 referring to a file. It checks whether the file exists. An example |
142 referring to a file. It checks whether the file exists. An example |
124 is |
143 is |
125 |
144 |
126 @{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>} |
145 @{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>} |
127 \end{itemize} |
146 \end{itemize} |
128 |
147 |
129 The listed antiquotations honour options including \<open>[display]\<close> and |
148 The listed antiquotations honour options including \<open>[display]\<close> and |
130 \<open>[quotes]\<close>. For example |
149 \<open>[gray]\<close>. For example |
131 |
150 |
132 \begin{center}\small |
|
133 \<open>@{ML [quotes] \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces\;\; @{text [quotes] "foobar"} |
|
134 \end{center} |
|
135 |
|
136 whereas |
|
137 |
|
138 \begin{center}\small |
|
139 \<open>@{ML \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces only\;\; \<open>foobar\<close> |
|
140 \end{center} |
|
141 |
151 |
142 \item Functions and value bindings cannot be defined inside antiquotations; they need |
152 \item Functions and value bindings cannot be defined inside antiquotations; they need |
143 to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> |
153 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 |
154 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
145 the tutorial, however, ensures that the environment markers are not printed. |
155 the tutorial, however, ensures that the environment markers are not printed. |