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/075bda98965195f522cf1de02aaf9a6f23d0b050
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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
