19
|
1 |
(* Title: Pure/install_pp.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
|
619
|
4 |
Set up automatic toplevel pretty printing.
|
0
|
5 |
*)
|
|
6 |
|
619
|
7 |
fun init_pps () =
|
|
8 |
use_string
|
1528
|
9 |
["install_pp (make_pp [\"Theory\", \"theory\"] pprint_theory);",
|
|
10 |
"install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
|
619
|
11 |
"install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);",
|
|
12 |
"install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);",
|
|
13 |
"install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);",
|
|
14 |
"install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);",
|
|
15 |
"install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"];
|
0
|
16 |
|
619
|
17 |
init_pps ();
|
254
|
18 |
|