ProgTutorial/Readme.thy
changeset 572 438703674711
parent 571 95b42288294e
child 573 321e220a6baa
--- a/ProgTutorial/Readme.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Readme.thy	Tue May 21 14:37:39 2019 +0200
@@ -90,7 +90,7 @@
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>}\<close>\\
+  \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>\<close>\\
                                & \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ 
   \<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ 
                                & \<open>\<open>Exception FAIL raised\<close>}\<close>
@@ -129,14 +129,42 @@
   \end{tabular}
   \end{center}
 
- which produce respectively
+ which produces
+
+  \begin{center}\small
+  @{ML_response \<open>1 upto 10\<close>}
+  \end{center}
+ 
+  You can give a second argument for the expected response. This is matched against the actual
+  response by crude wildcard matching where whitespace and \<open>\<dots>\<close> are treated as wildcard.
 
   \begin{center}\small
-  \begin{tabular}{p{3cm}p{3cm}}
-  @{ML_response \<open>1 upto 10\<close>}
+  \begin{tabular}{ll}
+  \<open>@{ML_response\<close> & \<open>\<open>1 upto 20\<close>\<close>\\
+                  & \<open>"[1, 2, 3, 4, 5, 6\<dots>\<close>\\
+                  &   \<open>18, 19, 20]"}\<close>\\
   \end{tabular}
   \end{center}
- 
+
+  will produce
+
+  @{ML_response \<open>1 upto 20\<close>
+\<open>[1, 2, 3, 4, 5, 6\<dots> 
+  18, 19, 20]\<close>}
+
+  Note that exceptions are also converted to strings and can thus be checked in the response 
+  string.
+
+  @{ML_response \<open>error "hallo"\<close>
+  \<open>hallo\<close>}
+
+So as a rule of thumb, to facilitate result checking use prefer this order:
+\begin{enumerate}
+ \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>
+ \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close>
+ \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close>
+ \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close>
+\end{enumerate}
 
   \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when
   referring to a file. It checks whether the file exists.  An example