88 |
86 |
89 The second antiquotation extends the first by allowing also to give |
87 The second antiquotation extends the first by allowing also to give |
90 hints what the result of the ML-code should be and to check the consistency of |
88 hints what the result of the ML-code should be and to check the consistency of |
91 the actual result with these hints. For this we are going to implement the |
89 the actual result with these hints. For this we are going to implement the |
92 antiquotation |
90 antiquotation |
93 @{text "@{ML_response \"expr\" \"pat\"}"} |
91 @{text "@{ML_resp \"expr\" \"pat\"}"} |
94 whose first argument is the ML-code and the second is a pattern specifying |
92 whose first argument is the ML-code and the second is a pattern specifying |
95 the result. To add some convenience and allow dealing with large outputs, |
93 the result. To add some convenience and allow dealing with large outputs, |
96 the user can give a partial specification including abbreviations |
94 the user can give a partial specification including abbreviations |
97 @{text [quotes] "\<dots>"}. |
95 @{text [quotes] "\<dots>"}. |
98 |
96 |
115 text {* |
113 text {* |
116 Next we like to add a response indicator to the result using: |
114 Next we like to add a response indicator to the result using: |
117 *} |
115 *} |
118 |
116 |
119 |
117 |
120 ML{*fun add_response_indicator pat = |
118 ML{*fun add_resp_indicator pat = |
121 map (fn s => "> " ^ s) (space_explode "\n" pat) *} |
119 map (fn s => "> " ^ s) (space_explode "\n" pat) *} |
122 |
120 |
123 text {* |
121 text {* |
124 The rest of the code of the antiquotation is |
122 The rest of the code of the antiquotation is |
125 *} |
123 *} |
126 |
124 |
127 ML{*fun output_ml_response src ctxt ((code_txt,pat),pos) = |
125 ML{*fun output_ml_resp src ctxt ((code_txt,pat),pos) = |
128 (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); |
126 (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); |
129 let |
127 let |
130 val output = (space_explode "\n" code_txt) @ (add_response_indicator pat) |
128 val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat) |
131 in |
129 in |
132 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output |
130 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output |
133 end) |
131 end) |
134 |
132 |
135 val _ = ThyOutput.add_commands |
133 val _ = ThyOutput.add_commands |
136 [("ML_response", |
134 [("ML_resp", |
137 ThyOutput.args |
135 ThyOutput.args |
138 (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
136 (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
139 output_ml_response)]*} |
137 output_ml_resp)]*} |
140 |
138 |
141 text {* |
139 text {* |
142 This extended antiquotation allows us to write |
140 This extended antiquotation allows us to write |
143 @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"} |
141 |
|
142 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |
|
143 |
144 to obtain |
144 to obtain |
145 |
145 |
146 @{ML_response [display] "true andalso false" "false"} |
146 @{ML_resp [display] "true andalso false" "false"} |
147 |
147 |
148 or |
148 or |
149 |
149 |
150 @{text [display] "@{ML_response [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"} |
150 @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"} |
151 |
151 |
152 to obtain |
152 to obtain |
153 |
153 |
154 @{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} |
154 @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} |
155 |
155 |
156 In both cases, the check by the compiler ensures that code and result match. A limitation |
156 In both cases, the check by the compiler ensures that code and result match. A limitation |
157 of this antiquotation is that the hints can only be given for results that can actually |
157 of this antiquotation is that the hints can only be given for results that can actually |
158 be constructed as a pattern. This excludes values that are abstract datatypes, like |
158 be constructed as a pattern. This excludes values that are abstract datatypes, like |
159 theorems or cterms. |
159 theorems or cterms. |