added init_pps;
authorwenzelm
Mon Sep 26 17:36:10 1994 +0100 (1994-09-26)
changeset 619a0342b27b38e
parent 618 97b715e65f70
child 620 f787eb061618
added init_pps;
src/Pure/install_pp.ML
     1.1 --- a/src/Pure/install_pp.ML	Mon Sep 26 17:35:45 1994 +0100
     1.2 +++ b/src/Pure/install_pp.ML	Mon Sep 26 17:36:10 1994 +0100
     1.3 @@ -1,19 +1,18 @@
     1.4  (*  Title:      Pure/install_pp.ML
     1.5      ID:         $Id$
     1.6  
     1.7 -Set up automatic toplevel printing.
     1.8 +Set up automatic toplevel pretty printing.
     1.9  *)
    1.10  
    1.11 -install_pp (make_pp ["Thm", "thm"] pprint_thm);
    1.12 -install_pp (make_pp ["Thm", "theory"] pprint_theory);
    1.13 -install_pp (make_pp ["Thm", "cterm"] pprint_cterm);
    1.14 -install_pp (make_pp ["Thm", "ctyp"] pprint_ctyp);
    1.15 -install_pp (make_pp ["Sign", "sg"] Sign.pprint_sg);
    1.16 -install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    1.17 -install_pp (make_pp ["typ"] Syntax.simple_pprint_typ);
    1.18 +fun init_pps () =
    1.19 +  use_string
    1.20 +   ["install_pp (make_pp [\"Thm\", \"thm\"] pprint_thm);",
    1.21 +    "install_pp (make_pp [\"Thm\", \"theory\"] pprint_theory);",
    1.22 +    "install_pp (make_pp [\"Thm\", \"cterm\"] pprint_cterm);",
    1.23 +    "install_pp (make_pp [\"Thm\", \"ctyp\"] pprint_ctyp);",
    1.24 +    "install_pp (make_pp [\"Sign\", \"sg\"] Sign.pprint_sg);",
    1.25 +    "install_pp (make_pp [\"Syntax\", \"ast\"] Syntax.pprint_ast);",
    1.26 +    "install_pp (make_pp [\"typ\"] Syntax.simple_pprint_typ);"];
    1.27  
    1.28 -(*
    1.29 -install_pp (make_pp ["term"] pprint_term);
    1.30 -install_pp (make_pp ["typ"] pprint_typ);
    1.31 -*)
    1.32 +init_pps ();
    1.33