On Mon, 12 Apr 2010, David Matthews wrote:
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.
OK, PolyML.prettyRepresentation looks like the right thing. Since Isabelle/ML has its own mechanism to inline code via antiquotations, we can easily retain the adhoc polymorphism involved here.
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.
If you really want to augment the functionality here, I would prefer a separate PrettyLineBreak constructor.
Makarius