src/Pure/install_pp.ML
author paulson
Fri, 01 Mar 1996 10:17:37 +0100
changeset 1528 608dd813b437
parent 619 a0342b27b38e
child 3509 db03a42120bf
permissions -rw-r--r--
Theories are now in theory.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/install_pp.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
619
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
     4
Set up automatic toplevel pretty printing.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
619
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
     7
fun init_pps () =
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
     8
  use_string
1528
608dd813b437 Theories are now in theory.ML
paulson
parents: 619
diff changeset
     9
   ["install_pp (make_pp [\"Theory\", \"theory\"] pprint_theory);",
608dd813b437 Theories are now in theory.ML
paulson
parents: 619
diff changeset
    10
    "install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
619
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
    11
    "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);",
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
    12
    "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);",
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
    13
    "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);",
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
    14
    "install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);",
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
    15
    "install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
619
a0342b27b38e added init_pps;
wenzelm
parents: 254
diff changeset
    17
init_pps ();
254
b1fcd27fcac4 replaced pprint_sg by Sign.pprint_sg;
wenzelm
parents: 230
diff changeset
    18