257 ML{*fun pretty_terms ctxt ts = |
257 ML{*fun pretty_terms ctxt ts = |
258 Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*} |
258 Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*} |
259 |
259 |
260 text {* |
260 text {* |
261 You can also print out terms together with their typing information. |
261 You can also print out terms together with their typing information. |
262 For this you need to set the reference @{ML_ind show_types in Syntax} |
262 For this you need to set the configuration value |
263 to @{ML true}. |
263 @{ML_ind show_types in Syntax} to @{ML true}. |
264 *} |
264 *} |
265 |
265 |
266 ML{*show_types := true*} |
266 ML{*val show_types_ctxt = Config.put show_types true @{context}*} |
267 |
267 |
268 text {* |
268 text {* |
269 Now @{ML pretty_term} prints out |
269 Now by using this context @{ML pretty_term} prints out |
270 |
270 |
271 @{ML_response_fake [display, gray] |
271 @{ML_response_fake [display, gray] |
272 "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})" |
272 "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})" |
273 "(1::nat, x::'a)"} |
273 "(1::nat, x::'a)"} |
274 |
274 |
275 where @{text 1} and @{text x} are displayed with their inferred type. |
275 where @{text 1} and @{text x} are displayed with their inferred type. |
276 Even more type information can be printed by setting |
276 Even more type information can be printed by setting |
277 the reference @{ML_ind show_all_types in Syntax} to @{ML true}. |
277 the reference @{ML_ind show_all_types in Syntax} to @{ML true}. |
278 In this case we obtain |
278 In this case we obtain |
279 *} |
279 *} |
280 (*<*)ML %linenos {*show_all_types := true*} |
280 |
281 (*>*) |
|
282 text {* |
281 text {* |
283 @{ML_response_fake [display, gray] |
282 @{ML_response_fake [display, gray] |
284 "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})" |
283 "pwriteln (pretty_term |
|
284 (Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})" |
285 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
285 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
286 |
286 |
287 where @{term Pair} is the term-constructor for products. |
287 where @{term Pair} is the term-constructor for products. |
288 Other references that influence printing of terms are |
288 Other configuration values that influence printing of terms are |
289 @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. |
289 @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. |
290 *} |
290 *} |
291 (*<*)ML %linenos {*show_types := false; show_all_types := false*} |
291 |
292 (*>*) |
|
293 text {* |
292 text {* |
294 A @{ML_type cterm} can be printed with the following function. |
293 A @{ML_type cterm} can be printed with the following function. |
295 *} |
294 *} |
296 |
295 |
297 ML{*fun pretty_cterm ctxt ct = |
296 ML{*fun pretty_cterm ctxt ct = |