equal
deleted
inserted
replaced
|
1 (* Title: Pure/install_pp |
|
2 ID: $Id$ |
|
3 |
|
4 Set up automatic toplevel printing |
|
5 *) |
|
6 |
|
7 install_pp (make_pp ["Thm", "thm"] pprint_thm); |
|
8 install_pp (make_pp ["Thm", "theory"] pprint_theory); |
|
9 install_pp (make_pp ["Sign", "sg"] pprint_sg); |
|
10 install_pp (make_pp ["term"] pprint_term); |
|
11 install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm); |
|
12 install_pp (make_pp ["typ"] pprint_typ); |
|
13 install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp); |
|
14 install_pp (make_pp ["Ast", "ast"] Syntax.pprint_ast); |
|
15 |