Makarius wrote:

Two questions concerning the builtin pretty printing facilities of Poly/ML 5.3 (or pre-5.4 SVN version 1125).

(1) The Poly/ML toplevel pretty prints values nicely, according to the print functions installed by the user. It seems that PolyML.print (and PolyML.makestring) produce an unformatted string only via PolyML.uglyPrint instead of PolyML.prettyPrint.

Is this a fundamental limitation, or could one get regular pretty printed output here as well?

PolyML.print uses the pretty-printer to format the output according to the line width set with PolyML.line_length. Only PolyML.makestring uses uglyprint. The idea is that makestring simply turns the output into an unformatted string. There's also PolyML.prettyRepresentation which takes any value and a "print depth" and returns the PolyML.pretty data structure. You could use this to produce a string in your own format but that wouldn't work if you wanted something that was polymorphic because you'd lose the "funny polymorphism" of PolyML.makestring.

(2) When mapping Pretty.fbrk (forced break) of Isabelle to the Poly/ML model we simulate it via a very large regular break, greater than the usual line length. This produces funny output with PolyML.print/makestring, because it does not do the formatting as observed above.

It looks like there's a bug in the pretty printer that causes it not to break properly in these circumstances. It looks like it should be easy to fix.

Is it possible to force breaks more directly, apart from embedding a literal "\n" which is not counted properly?

There are various possibilities. I could add a PrettyLineBreak constructor to the pretty datatype or interpret values such as "\n" within a string as a line break.

David