equal
deleted
inserted
replaced
31 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
31 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
32 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; |
32 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; |
33 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; |
33 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; |
34 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; |
34 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; |
35 |
35 |
36 if ml_system = "polyml-experimental" |
36 if ml_system = "polyml-5.3.0" |
37 then use "ML-Systems/install_pp_polyml-5.3.ML" |
37 then use "ML-Systems/install_pp_polyml-5.3.ML" |
38 else if String.isPrefix "polyml" ml_system |
38 else if String.isPrefix "polyml" ml_system |
39 then use "ML-Systems/install_pp_polyml.ML" |
39 then use "ML-Systems/install_pp_polyml.ML" |
40 else (); |
40 else (); |
41 |
41 |