253 ML{*fun string_of_terms ctxt ts = |
253 ML{*fun string_of_terms ctxt ts = |
254 commas (map (string_of_term ctxt) ts)*} |
254 commas (map (string_of_term ctxt) ts)*} |
255 |
255 |
256 text {* |
256 text {* |
257 Sometimes you want to print out a term together with some type information. |
257 Sometimes you want to print out a term together with some type information. |
258 This can be achieved by setting the reference |
258 This can be achieved by setting the reference @{ML_ind show_types in Syntax} |
259 @{ML_ind show_types}\footnote{\bf FIXME: ``forgotten'' structure Printer, Mixfix etc.} |
|
260 to @{ML true}. |
259 to @{ML true}. |
261 *} |
260 *} |
262 |
261 |
263 ML{*show_types := true*} |
262 ML{*show_types := true*} |
264 |
263 |
269 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
268 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
270 "(1::nat, x::'a)"} |
269 "(1::nat, x::'a)"} |
271 |
270 |
272 where @{text 1} and @{text x} are displayed with their type. |
271 where @{text 1} and @{text x} are displayed with their type. |
273 Even more type information can be printed by setting |
272 Even more type information can be printed by setting |
274 @{ML_ind show_all_types} to @{ML true}. We obtain |
273 @{ML_ind show_all_types in Syntax} to @{ML true}. We obtain |
275 *} |
274 *} |
276 (*<*)ML %linenos {*show_all_types := true*} |
275 (*<*)ML %linenos {*show_all_types := true*} |
277 (*>*) |
276 (*>*) |
278 text {* |
277 text {* |
279 @{ML_response_fake [display, gray] |
278 @{ML_response_fake [display, gray] |
280 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
279 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
281 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
280 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
282 |
281 |
283 Other references that influence printing are @{ML_ind show_brackets} |
282 Other references that influence printing are @{ML_ind show_brackets in Syntax} |
284 and @{ML_ind show_sorts}. |
283 and @{ML_ind show_sorts in Syntax}. |
285 *} |
284 *} |
286 (*<*)ML %linenos {*show_types := false; show_all_types := false*} |
285 (*<*)ML %linenos {*show_types := false; show_all_types := false*} |
287 (*>*) |
286 (*>*) |
288 text {* |
287 text {* |
289 A @{ML_type cterm} can be transformed into a string by the following function. |
288 A @{ML_type cterm} can be transformed into a string by the following function. |