diff -r 95b42288294e -r 438703674711 ProgTutorial/Readme.thy --- 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} - \@{ML_matchresult_fake\ & \\term_of @{theory} @{term "a + b = c"}\}\\\ + \@{ML_matchresult_fake\ & \\term_of @{theory} @{term "a + b = c"}\\\\ & \\a + b = c\}\\smallskip\\ \@{ML_matchresult_fake\ & \\($$ "x") (explode "world")\\\\ & \\Exception FAIL raised\}\ @@ -129,14 +129,42 @@ \end{tabular} \end{center} - which produce respectively + which produces + + \begin{center}\small + @{ML_response \1 upto 10\} + \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 \\\ are treated as wildcard. \begin{center}\small - \begin{tabular}{p{3cm}p{3cm}} - @{ML_response \1 upto 10\} + \begin{tabular}{ll} + \@{ML_response\ & \\1 upto 20\\\\ + & \"[1, 2, 3, 4, 5, 6\\\\ + & \18, 19, 20]"}\\\ \end{tabular} \end{center} - + + will produce + + @{ML_response \1 upto 20\ +\[1, 2, 3, 4, 5, 6\ + 18, 19, 20]\} + + Note that exceptions are also converted to strings and can thus be checked in the response + string. + + @{ML_response \error "hallo"\ + \hallo\} + +So as a rule of thumb, to facilitate result checking use prefer this order: +\begin{enumerate} + \item \@{ML_matchresult \expr\ \pat\}\ + \item \@{ML_response \expr\ \string\}\ + \item \@{ML_matchresult_fake \expr\ \pat\}\ or \@{ML_response \expr\}\ + \item \@{ML_matchresult_fake_both \expr\ \pat\}\ +\end{enumerate} \item[$\bullet$] \@{ML_file "name"}\ should be used when referring to a file. It checks whether the file exists. An example