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