src/Pure/pure_setup.ML
changeset 37858 e1ef6b441fe7
parent 37535 75de61a479e3
child 37860 aa3b3d00698b
equal deleted inserted replaced
37857:4e4b8c0dc766 37858:e1ef6b441fe7
    32 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
    32 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
    33 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    33 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    34 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
    34 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
    35 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
    35 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
    36 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
    36 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
       
    37 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
       
    38 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    37 
    39 
    38 if ml_system = "polyml-5.3.0"
    40 if ml_system = "polyml-5.3.0"
    39 then use "ML-Systems/install_pp_polyml-5.3.ML"
    41 then use "ML-Systems/install_pp_polyml-5.3.ML"
    40 else if String.isPrefix "polyml" ml_system
    42 else if String.isPrefix "polyml" ml_system
    41 then use "ML-Systems/install_pp_polyml.ML"
    43 then use "ML-Systems/install_pp_polyml.ML"