On Mon, 14 Dec 2009, Rob Arthan wrote:
For what it is worth, I have attached a patch that fixes PolyML.install_pp. On reflection, if you withdraw it, I am going to have to write something similar of my own, because I can't see any other way of maintaining compatibility with both Poly/ML and SML/NJ.
IIRC, you are using a version of our former make_pp/install_pp scheme. For Poly/ML 5.3 we've changed that to use the new PolyML.addPrettyPrinter, which also provides a few conveniences that old PolyML.install_pp lacks.
Nonetheless, we still need to support SML/NJ, and some older versions of Poly/ML. Since PolyML.install_pp is one of these special overloaded operations that cannot be rebound within the ML environment (apart from "open PolyML") without fixing its type once an for all, a different trick was required.
See our definition of toplevel_pp, which is now based on runtime compiler invocation via use_text:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-1/src/Pure/ML-Sys... http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-1/src/Pure/ML-Sys...
Here are some examples that work for all SML compilers supported by Isabelle2009-1:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-1/src/Pure/pure_s...
Apart from that we now have some advanced pretty printers that only work with Poly/ML 5.3:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-1/src/Pure/ML-Sys...
(The one for datatype term is needed, because our infix constructor "$" would be printed in prefix notation by Poly/ML 5.3.)
The overall situation has definitely become a bit more complex than 10-15 years ago, but there are also some significant improvements in the new scheme. E.g. we can pass additional properties through the pp output, without affecting indentation produced by Poly/ML. This allows to pass our own position information and additional markup, which will become particularly important in the coming post-tty interface era.
Makarius