252 |
252 |
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. |
|
258 This can be achieved by setting the reference |
|
259 @{ML_ind show_types}\footnote{\bf FIXME: ``forgotten'' structure Printer, Mixfix etc.} |
|
260 to @{ML true}. |
|
261 *} |
|
262 |
|
263 ML{*show_types := true*} |
|
264 |
|
265 text {* |
|
266 Now @{ML string_of_term} prints out |
|
267 |
|
268 @{ML_response_fake [display, gray] |
|
269 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
|
270 "(1::nat, x::'a)"} |
|
271 |
|
272 where @{text 1} and @{text x} are displayed with their type. |
|
273 Even more type information can be printed by setting |
|
274 @{ML_ind show_all_types} to @{ML true}. We obtain |
|
275 *} |
|
276 (*<*)ML %linenos {*show_all_types := true*} |
|
277 (*>*) |
|
278 text {* |
|
279 @{ML_response_fake [display, gray] |
|
280 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" |
|
281 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
|
282 |
|
283 Other references that influence printing are @{ML_ind show_brackets} |
|
284 and @{ML_ind show_sorts}. |
|
285 *} |
|
286 (*<*)ML %linenos {*show_types := false; show_all_types := false*} |
|
287 (*>*) |
|
288 text {* |
257 A @{ML_type cterm} can be transformed into a string by the following function. |
289 A @{ML_type cterm} can be transformed into a string by the following function. |
258 *} |
290 *} |
259 |
291 |
260 ML{*fun string_of_cterm ctxt ct = |
292 ML{*fun string_of_cterm ctxt ct = |
261 string_of_term ctxt (term_of ct)*} |
293 string_of_term ctxt (term_of ct)*} |
319 |
351 |
320 fun string_of_thms_no_vars ctxt thms = |
352 fun string_of_thms_no_vars ctxt thms = |
321 commas (map (string_of_thm_no_vars ctxt) thms) *} |
353 commas (map (string_of_thm_no_vars ctxt) thms) *} |
322 |
354 |
323 text {* |
355 text {* |
|
356 \begin{readmore} |
|
357 The simple conversion functions from Isabelle's main datatypes to |
|
358 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. |
|
359 The references that change the printing information are declared in |
|
360 @{ML_file "Pure/Syntax/printer.ML"}. |
|
361 \end{readmore} |
|
362 |
324 Note that when printing out several ``parcels'' of information that |
363 Note that when printing out several ``parcels'' of information that |
325 semantically belong together, like a warning message consisting of |
364 semantically belong together, like a warning message consisting of |
326 a term and its type, you should try to keep this information together in a |
365 a term and its type, you should try to keep this information together in a |
327 single string. Therefore do \emph{not} print out information as |
366 single string. Therefore do \emph{not} print out information as |
328 |
367 |