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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
