equal
deleted
inserted
replaced
171 let val s = implode_path path |
171 let val s = implode_path path |
172 in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; |
172 in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; |
173 |
173 |
174 val print = Pretty.unformatted_string_of o pretty; |
174 val print = Pretty.unformatted_string_of o pretty; |
175 |
175 |
176 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty); |
176 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); |
177 |
177 |
178 |
178 |
179 (* base element *) |
179 (* base element *) |
180 |
180 |
181 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) |
181 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) |