248 @{ML_response_fake [display,gray] |
248 @{ML_response_fake [display,gray] |
249 "pwriteln (pretty_term @{context} @{term \"1::nat\"})" |
249 "pwriteln (pretty_term @{context} @{term \"1::nat\"})" |
250 "\"1\""} |
250 "\"1\""} |
251 |
251 |
252 If there is more than one term to be printed, you can use the |
252 If there is more than one term to be printed, you can use the |
253 function @{ML_ind enum in Pretty} and commas to separate them. |
253 function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} |
|
254 to separate them. |
254 *} |
255 *} |
255 |
256 |
256 ML{*fun pretty_terms ctxt ts = |
257 ML{*fun pretty_terms ctxt ts = |
257 Pretty.enum "," "" "" (map (pretty_term ctxt) ts)*} |
258 Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*} |
258 |
259 |
259 text {* |
260 text {* |
260 You can also print out terms together with their typing information. |
261 You can also print out terms together with their typing information. |
261 For this you need to set the reference @{ML_ind show_types in Syntax} |
262 For this you need to set the reference @{ML_ind show_types in Syntax} |
262 to @{ML true}. |
263 to @{ML true}. |
297 pretty_term ctxt (term_of ct)*} |
298 pretty_term ctxt (term_of ct)*} |
298 |
299 |
299 text {* |
300 text {* |
300 Here the function @{ML_ind term_of in Thm} extracts the @{ML_type |
301 Here the function @{ML_ind term_of in Thm} extracts the @{ML_type |
301 term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be |
302 term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be |
302 printed again with @{ML enum in Pretty}. |
303 printed again with @{ML commas in Pretty}. |
303 *} |
304 *} |
304 |
305 |
305 ML{*fun pretty_cterms ctxt cts = |
306 ML{*fun pretty_cterms ctxt cts = |
306 Pretty.enum "," "" "" (map (pretty_cterm ctxt) cts)*} |
307 Pretty.block (Pretty.commas (map (pretty_cterm ctxt) cts))*} |
307 |
308 |
308 text {* |
309 text {* |
309 The easiest way to get the string of a theorem is to transform it |
310 The easiest way to get the string of a theorem is to transform it |
310 into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. |
311 into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. |
311 *} |
312 *} |
350 |
351 |
351 Again the function @{ML commas} helps with printing more than one theorem. |
352 Again the function @{ML commas} helps with printing more than one theorem. |
352 *} |
353 *} |
353 |
354 |
354 ML{*fun pretty_thms ctxt thms = |
355 ML{*fun pretty_thms ctxt thms = |
355 Pretty.enum "," "" "" (map (pretty_thm ctxt) thms) |
356 Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms)) |
356 |
357 |
357 fun pretty_thms_no_vars ctxt thms = |
358 fun pretty_thms_no_vars ctxt thms = |
358 Pretty.enum "," "" "" (map (pretty_thm_no_vars ctxt) thms)*} |
359 Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*} |
359 |
360 |
360 text {* |
361 text {* |
361 The printing functions for types are |
362 The printing functions for types are |
362 *} |
363 *} |
363 |
364 |
364 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty |
365 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty |
365 fun pretty_typs ctxt tys = Pretty.commas (map (pretty_typ ctxt) tys)*} |
366 fun pretty_typs ctxt tys = |
|
367 Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*} |
366 |
368 |
367 text {* |
369 text {* |
368 respectively ctypes |
370 respectively ctypes |
369 *} |
371 *} |
370 |
372 |
371 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty) |
373 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty) |
372 fun pretty_ctyps ctxt ctys = Pretty.commas (map (pretty_ctyp ctxt) ctys)*} |
374 fun pretty_ctyps ctxt ctys = |
|
375 Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*} |
373 |
376 |
374 text {* |
377 text {* |
375 \begin{readmore} |
378 \begin{readmore} |
376 The simple conversion functions from Isabelle's main datatypes to |
379 The simple conversion functions from Isabelle's main datatypes to |
377 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. |
380 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. |