src/Pure/General/path.ML

   let val s = implode_path path
   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
 
 val print = Pretty.unformatted_string_of o pretty;
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+
 
 (* base element *)
 
 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
   | split_path _ path = error ("Cannot split path into dir/base: " ^ print path);