Rob, I think the problem is actually with the wrapper function that is used to emulate install_pp in terms of addPrettyPrinter. When I wrote a version of your pretty printer directly in the new form (included below) it worked as expected. I've now written a quick document describing the new pretty printer ( http://www.polyml.org/docs/PrettyPrint.html ) so it might be easier to convert your pretty printers if possible. I'll try and see if I can fix install_pp but it's currently broken in SVN because of some other changes. Regards, David
datatype TERM = Num of int | Plus of TERM * TERM;
local open PolyML fun term_pp depth unused (t: TERM) = case t of Num n => PrettyString (Int.toString n) | Plus (t1, t2) => PrettyBlock(0, true, [], [ term_pp depth unused t1, PrettyBreak(1, 0), PrettyString "+", PrettyBreak(1, 0), term_pp depth unused t2 ]) in fun pp flag depth unused t = PrettyBlock(0, flag, [], [ PrettyBlock(0, false, [], [term_pp depth unused (t: TERM)]) ]) end; fun interval m n = ( let fun aux acc i = ( if i < m then acc else aux (i::acc) (i-1) ); in aux [] n end ); PolyML.Compiler.lineLength := 40; val _ = PolyML.addPrettyPrinter (pp false); val t = foldr Plus (Num 0) (map Num (interval 1 40));
val _ = PolyML.addPrettyPrinter (pp true); t;
Rob Arthan wrote:
I can't find any documentation for the new approach to pretty-printing in version 5.3 of Poly/ML. For ProofPower, I am using the PolyML.install_pp interface that is provided for backwards compatibility. but it doesn't seem to give the same results. I find that many things that used to print nicely spread over several lines now print as one long thin column with only one or two symbols in each column.
The problem seems to be with the interpretation of the boolean part of the parameter to the function that begins a block. The attached code shows a difference between 5.2 and 5.3. On 5.2 both times the value of t t is pretty-printed you get the same results, which is one symbol per line until what is left will fit all on one line. On 5.3, the first time you get a sqaureish block and the second time you get one symbol per line.
I can't find any documentation for the install_pp interface either so I don't really know which behaviour is right.
Regards,