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,
Rob.
datatype TERM = Num of int | Plus of TERM * TERM; fun term_pp (funs as ( adds : string -> unit, beginb : int * bool -> unit, space : int * int -> unit, endb : unit -> unit)) (t : TERM) = ( case t of Num n => adds (Int.toString n) | Plus (t1, t2) => ( beginb(0, true); term_pp funs t1; space(1, 0); adds "+"; space(1, 0); term_pp funs t2; endb() ) ); fun pp flag (funs as (adds, beginb, space, endb)) _ _ t = ( beginb(0, flag); beginb(0, false); (* removing this and the matching end makes no difference *) term_pp funs t; endb(); endb() ); 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.install_pp (pp false); val t = foldr Plus (Num 0) (map Num (interval 1 40));
val _ = PolyML.install_pp (pp true); t;