88 when the result cannot be constructed or the code generates an |
88 when the result cannot be constructed or the code generates an |
89 exception. Examples are: |
89 exception. Examples are: |
90 |
90 |
91 \begin{center}\small |
91 \begin{center}\small |
92 \begin{tabular}{ll} |
92 \begin{tabular}{ll} |
93 \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>}\<close>\\ |
93 \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>\<close>\\ |
94 & \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ |
94 & \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ |
95 \<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ |
95 \<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ |
96 & \<open>\<open>Exception FAIL raised\<close>}\<close> |
96 & \<open>\<open>Exception FAIL raised\<close>}\<close> |
97 \end{tabular} |
97 \end{tabular} |
98 \end{center} |
98 \end{center} |
127 \begin{tabular}{ll} |
127 \begin{tabular}{ll} |
128 \<open>@{ML_response\<close> & \<open>\<open>1 upto 10\<close>}\<close> |
128 \<open>@{ML_response\<close> & \<open>\<open>1 upto 10\<close>}\<close> |
129 \end{tabular} |
129 \end{tabular} |
130 \end{center} |
130 \end{center} |
131 |
131 |
132 which produce respectively |
132 which produces |
133 |
133 |
134 \begin{center}\small |
134 \begin{center}\small |
135 \begin{tabular}{p{3cm}p{3cm}} |
|
136 @{ML_response \<open>1 upto 10\<close>} |
135 @{ML_response \<open>1 upto 10\<close>} |
|
136 \end{center} |
|
137 |
|
138 You can give a second argument for the expected response. This is matched against the actual |
|
139 response by crude wildcard matching where whitespace and \<open>\<dots>\<close> are treated as wildcard. |
|
140 |
|
141 \begin{center}\small |
|
142 \begin{tabular}{ll} |
|
143 \<open>@{ML_response\<close> & \<open>\<open>1 upto 20\<close>\<close>\\ |
|
144 & \<open>"[1, 2, 3, 4, 5, 6\<dots>\<close>\\ |
|
145 & \<open>18, 19, 20]"}\<close>\\ |
137 \end{tabular} |
146 \end{tabular} |
138 \end{center} |
147 \end{center} |
139 |
148 |
|
149 will produce |
|
150 |
|
151 @{ML_response \<open>1 upto 20\<close> |
|
152 \<open>[1, 2, 3, 4, 5, 6\<dots> |
|
153 18, 19, 20]\<close>} |
|
154 |
|
155 Note that exceptions are also converted to strings and can thus be checked in the response |
|
156 string. |
|
157 |
|
158 @{ML_response \<open>error "hallo"\<close> |
|
159 \<open>hallo\<close>} |
|
160 |
|
161 So as a rule of thumb, to facilitate result checking use prefer this order: |
|
162 \begin{enumerate} |
|
163 \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> |
|
164 \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close> |
|
165 \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close> |
|
166 \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close> |
|
167 \end{enumerate} |
140 |
168 |
141 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
169 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
142 referring to a file. It checks whether the file exists. An example |
170 referring to a file. It checks whether the file exists. An example |
143 is |
171 is |
144 |
172 |