4 Set up automatic toplevel pretty printing. |
4 Set up automatic toplevel pretty printing. |
5 *) |
5 *) |
6 |
6 |
7 fun init_pps () = |
7 fun init_pps () = |
8 use_string |
8 use_string |
9 ["install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);", |
9 ["install_pp (make_pp [\"Theory\", \"theory\"] pprint_theory);", |
10 "install_pp (make_pp [\"Thm\", \"theory\"] pprint_theory);", |
10 "install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);", |
11 "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);", |
11 "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);", |
12 "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);", |
12 "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);", |
13 "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);", |
13 "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);", |
14 "install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);", |
14 "install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);", |
15 "install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"]; |
15 "install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"]; |