Generalise pretty-printers (allowing user implementation thereof).

This is "object oriented" in style: the user can provide an
implementation of the core API to create something of type ppstream.

I think this is necessary to better connect the HOL pretty-printer to the Poly/ML one.