52 \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\ |
52 \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\ |
53 \<open>@{ML Ident in OuterLex}\<close> & & @{ML Ident in OuterLex}\\ |
53 \<open>@{ML Ident in OuterLex}\<close> & & @{ML Ident in OuterLex}\\ |
54 \end{tabular} |
54 \end{tabular} |
55 \end{center} |
55 \end{center} |
56 |
56 |
57 \item[$\bullet$] \<open>@{ML_response "expr" "pat"}\<close> should be used to |
57 \item[$\bullet$] \<open>@{ML_matchresult "expr" "pat"}\<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 "expr"}\<close>; the second is a pattern |
59 like in the antiquotation \<open>@{ML "expr"}\<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] "\<dots>"} for parts that you like to omit. The response of the |
62 first expression will be checked against this pattern. Examples are: |
62 first expression will be checked against this pattern. Examples are: |
63 |
63 |
64 \begin{center}\small |
64 \begin{center}\small |
65 \begin{tabular}{l} |
65 \begin{tabular}{l} |
66 \<open>@{ML_response "1+2" "3"}\<close>\\ |
66 \<open>@{ML_matchresult "1+2" "3"}\<close>\\ |
67 \<open>@{ML_response "(1+2,3)" "(3,\<dots>)"}\<close> |
67 \<open>@{ML_matchresult "(1+2,3)" "(3,\<dots>)"}\<close> |
68 \end{tabular} |
68 \end{tabular} |
69 \end{center} |
69 \end{center} |
70 |
70 |
71 which produce respectively |
71 which produce respectively |
72 |
72 |
73 \begin{center}\small |
73 \begin{center}\small |
74 \begin{tabular}{p{3cm}p{3cm}} |
74 \begin{tabular}{p{3cm}p{3cm}} |
75 @{ML_response "1+2" "3"} & |
75 @{ML_matchresult "1+2" "3"} & |
76 @{ML_response "(1+2,3)" "(3,\<dots>)"} |
76 @{ML_matchresult "(1+2,3)" "(3,\<dots>)"} |
77 \end{tabular} |
77 \end{tabular} |
78 \end{center} |
78 \end{center} |
79 |
79 |
80 Note that this antiquotation can only be used when the result can be |
80 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 |
81 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}). |
82 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
83 |
83 |
84 \item[$\bullet$] \<open>@{ML_response_fake "expr" "pat"}\<close> works just |
84 \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just |
85 like the antiquotation \<open>@{ML_response "expr" "pat"}\<close> above, |
85 like the antiquotation \<open>@{ML_matchresult "expr" "pat"}\<close> above, |
86 except that the result-specification is not checked. Use this antiquotation |
86 except that the result-specification is not checked. Use this antiquotation |
87 when the result cannot be constructed or the code generates an |
87 when the result cannot be constructed or the code generates an |
88 exception. Examples are: |
88 exception. Examples are: |
89 |
89 |
90 \begin{center}\small |
90 \begin{center}\small |
91 \begin{tabular}{ll} |
91 \begin{tabular}{ll} |
92 \<open>@{ML_response_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\ |
92 \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\ |
93 & \<open>"a + b = c"}\<close>\smallskip\\ |
93 & \<open>"a + b = c"}\<close>\smallskip\\ |
94 \<open>@{ML_response_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ |
94 \<open>@{ML_matchresult_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ |
95 & \<open>"Exception FAIL raised"}\<close> |
95 & \<open>"Exception FAIL raised"}\<close> |
96 \end{tabular} |
96 \end{tabular} |
97 \end{center} |
97 \end{center} |
98 |
98 |
99 which produce respectively |
99 which produce respectively |
100 |
100 |
101 \begin{center}\small |
101 \begin{center}\small |
102 \begin{tabular}{p{7.2cm}} |
102 \begin{tabular}{p{7.2cm}} |
103 @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\ |
103 @{ML_matchresult_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\ |
104 @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"} |
104 @{ML_matchresult_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"} |
105 \end{tabular} |
105 \end{tabular} |
106 \end{center} |
106 \end{center} |
107 |
107 |
108 This output mimics to some extend what the user sees when running the |
108 This output mimics to some extend what the user sees when running the |
109 code. |
109 code. |
110 |
110 |
111 \item[$\bullet$] \<open>@{ML_response_fake_both "expr" "pat"}\<close> can be |
111 \item[$\bullet$] \<open>@{ML_matchresult_fake_both "expr" "pat"}\<close> can be |
112 used to show erroneous code. Neither the code nor the response will be |
112 used to show erroneous code. Neither the code nor the response will be |
113 checked. An example is: |
113 checked. An example is: |
114 |
114 |
115 \begin{center}\small |
115 \begin{center}\small |
116 \begin{tabular}{ll} |
116 \begin{tabular}{ll} |
117 \<open>@{ML_response_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\ |
117 \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\ |
118 & \<open>"Type unification failed \<dots>"}\<close> |
118 & \<open>"Type unification failed \<dots>"}\<close> |
119 \end{tabular} |
119 \end{tabular} |
120 \end{center} |
120 \end{center} |
121 |
121 |
122 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
122 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |