Rob,
On 07/01/2016 17:50, Rob Arthan wrote:
I was wrong about this. Later releases of ProofPower make some use of addPrettyPrinter but still use install_pp. I must have reverted to an earlier version of Poly/ML by mistake and thought things were working under Poly/ML 5.6, when they do not. Not having install_pp will be a stopper for me unless I can roll my own implementation of it using PolyML.addPrettyPrinter. Is that going to be an easy exercise?
The compatibility code for install_pp was removed with a commit on 19th October. See https://github.com/polyml/polyml/commit/075bda98965195f522cf1de02aaf9a6f23d0...
It should give you an idea of what to do but it's very simple because there's a close approximation between the old addString/beginBlock/break/endBlock and PrettyString, PrettyBlock and PrettyBreak. Essentially what it does is create a stack of pending beginBlocks and then adds the breaks and strings to the top of the stack, popping the stack when it finds an endBlock.
You'll have to convert each occurrence of install_pp individually because addPrettyPrinter and the old install_pp are type-dependent functions rather than polymorphic (like PolyML.print).
David