34 toplevel_pp ["Context", "theory"] "Context.pretty_thy"; |
34 toplevel_pp ["Context", "theory"] "Context.pretty_thy"; |
35 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
35 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
36 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
36 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
37 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; |
37 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; |
38 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; |
38 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; |
39 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; |
39 toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident"; |
40 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")"; |
40 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")"; |
41 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; |
41 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; |
42 |
42 |
43 if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" |
43 if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" |
44 then use "ML/install_pp_polyml.ML" |
44 then use "ML/install_pp_polyml.ML" |