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;
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,
David,
Thanks for responding so promptly with documentation for the new scheme. I have a query about this extract from your document:
"The consistent parameter indicates whether the block is to be broken consistently (true) or not (false). If it is true then if the block will not all fit on a line and must be broken then it will be broken at all the breaks in the block whether this is necessary or not."
I think "all the breaks in the block" here is intended to means all the PrettyBreak constructs appearing as immediate children of the PrettyBlock construct (so that nested PrettyBlock constructs override the outer setting of the consistent parameter). Is that right?
Regards,
Rob.
David Matthews wrote:
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,
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Rob Arthan wrote:
Thanks for responding so promptly with documentation for the new scheme. I have a query about this extract from your document:
"The consistent parameter indicates whether the block is to be broken consistently (true) or not (false). If it is true then if the block will not all fit on a line and must be broken then it will be broken at all the breaks in the block whether this is necessary or not."
I think "all the breaks in the block" here is intended to means all the PrettyBreak constructs appearing as immediate children of the PrettyBlock construct (so that nested PrettyBlock constructs override the outer setting of the consistent parameter). Is that right?
Yes. I wrote that rather quickly. It needs going through and rephrasing in some parts. If a nested block fits on a line then it is treated as a unit. I seem to recall, though, that if a nested block has to be broken because it won't fit then this causes breaks at all consistent breaks (i.e. breaks immediately within a block defined as consistent) in all outer blocks. It's a while since I looked at this.
Regards, David
David,
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.
Regards,
Rob.
Rob,
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.
I realised that the bug was in the beginBlock function and I committed a fix to 5.4 an hour or so ago. Was there a reason for the other changes that weren't fixed by that? If we can agree on a small set of changes I'll include them in the fixes-5.3 branch.
Regards, David
On 14 Dec 2009, at 18:33, David Matthews wrote:
Rob,
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.
I realised that the bug was in the beginBlock function and I committed a fix to 5.4 an hour or so ago. Was there a reason for the other changes that weren't fixed by that? If we can agree on a small set of changes I'll include them in the fixes-5.3 branch.
The old interface did not require a sequence of calls to the side-effecting functions to begin with a beginBlock and end with the matching endBlock. I think that what you have will raise an exception if this is not the case and if there is more than one call. My changes allow for a sequence of calls corresponding to a "pretty list" in the new regime rather than a single "pretty".
On thinking about this some more, I realise that some of the large applications QinetiQ tackle may suffer performance problems because of the list appends in addEntry. If it is not too much trouble, I think it would be prudent to construct the "pretty list"s backwards and reverse them when an entry is popped off the stack or extracted at the end.
Regards, Rob.
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
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
rda＠lemma-one.com