--- 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