On Fri, 23 Aug 2013, Michael Norrish wrote:
I'm a bit concerned that the new, recommended approach to pretty-printing requires me to translate into the Pretty structure before anything happens. I'd feel more comfortable if the structure could be produced and consumed lazily so that I don't end up with a large (strictly unnecessary) Pretty structure in memory.
What is "large" here? 64KB? 64MB? 64GB? As far as I know, the original Oppen paper was optimizing for some situation < 64KB. BTW Poly/ML does implicit sharing of subtree structures whenever you run short of heap space.
For my part, I welcome the way David Matthews has brushed up the toplevel pretty printing some time ago, to get away from this implicit stateful streaming. What is particularly nice is PolyML.ContextProperty, which allows to inject uninterpreted proper lists into the tree structure, and pick them up later for user-space interpretation. Thus it is possible to roll-your-own ML pretty printing -- the system merely passes certain tree structures through the toplevel infrastructure.
The only bottle neck encountered here is the 64 MB limit of strings: Isabelle insists in shipping the final result as one blob, and at that point it might crash with exception Size. This is just a historical accident of the Isabelle output functions to produce a single string in the end. It would be better to retain the pretty trees until the data is shipped to the external consumer, i.e. the Isabelle/Scala process that does the physical pretty printing wrt. font metrics and window sizes.
Makarius