User pretty-printers don't print via the formatter argument

[GoogleCodeExporter]

This causes user pretty-printers to print directly to the console, instead of 
the correct destination known to the formatter (e.g., a target string in 
string_of_term).

I attach a patchfile that fixes this that can be applied using the command 

patch -p0 < patchfile

Note: it changes the type of user pretty-printers by adding the formatter as an 
argument, so existing user pretty-printers will need to be updated.

Original issue reported on code.google.com by joe.h...@gmail.com on 3 Mar 2014 at 12:31

Attachments:

• patchfile

[GoogleCodeExporter]

Thanks, this has been incorporated in r184

Original comment by jrh...@gmail.com on 10 Mar 2014 at 4:59