| author | wenzelm |
| Fri, 20 Jul 2007 00:01:40 +0200 | |
| changeset 23877 | 307f75aaefca |
| parent 23873 | 6c644d14d91d |
| permissions | -rw-r--r-- |
| 19 | 1 |
(* Title: Pure/install_pp.ML |
| 0 | 2 |
ID: $Id$ |
3 |
||
|
16438
1093f2400411
removed obsolete pretty printers for Theory.theory, Sign.sg;
wenzelm
parents:
16355
diff
changeset
|
4 |
ML toplevel pretty printing. |
| 0 | 5 |
*) |
6 |
||
| 20211 | 7 |
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
8 |
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
|
9 |
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
|
|
16438
1093f2400411
removed obsolete pretty printers for Theory.theory, Sign.sg;
wenzelm
parents:
16355
diff
changeset
|
10 |
install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
| 20211 | 11 |
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
| 3509 | 12 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
| 20211 | 13 |
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy)); |
| 23877 | 14 |
install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode)); |
15 |
install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident)); |