equal
deleted
inserted
replaced
173 fun toplevel_pp context (_: string list) pp = |
173 fun toplevel_pp context (_: string list) pp = |
174 use_text context (1, "pp") false |
174 use_text context (1, "pp") false |
175 ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
175 ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
176 |
176 |
177 val ml_make_string = |
177 val ml_make_string = |
178 "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))"; |
178 "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))"; |
179 |
179 |