Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread Rob Arthan
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 mai

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread Makarius
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 SM

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread David Matthews
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 realis

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread Rob Arthan
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. --- mlsou

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread David Matthews
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 a

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread Rob Arthan
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

Re: [polyml] Pretty-printing in version 5.3

2009-12-14 Thread David Matthews
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

[polyml] Pretty-printing in version 5.3

2009-12-13 Thread Rob Arthan
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 nic