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