author | wenzelm |
Thu, 09 Jun 2005 16:58:03 +0200 | |
changeset 16355 | 06059ee940b6 |
parent 15633 | 741deccec4e3 |
child 16438 | 1093f2400411 |
permissions | -rw-r--r-- |
19 | 1 |
(* Title: Pure/install_pp.ML |
0 | 2 |
ID: $Id$ |
3 |
||
619 | 4 |
Set up automatic toplevel pretty printing. |
0 | 5 |
*) |
6 |
||
16355
06059ee940b6
full Display.pprint_theory for ML toplevel facilitates debugging;
wenzelm
parents:
15633
diff
changeset
|
7 |
install_pp (make_pp ["Theory", "theory"] Display.pprint_theory); |
11885 | 8 |
install_pp (make_pp ["Thm", "thm"] Display.pprint_thm); |
9 |
install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm); |
|
10 |
install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp); |
|
3509 | 11 |
install_pp (make_pp ["Sign", "sg"] Sign.pprint_sg); |
12 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
|
13 |
install_pp (make_pp ["typ"] Syntax.simple_pprint_typ); |