Support truncation metrics in the pretty printer module

[GoogleCodeExporter]

Allow the rendering of a pretty-printed document to be truncated when a limit 
of some kind is reached. Possible limits might be based on the number of 
characters or words or lines rendered.

Original issue reported on code.google.com by inkytonik on 22 Jan 2013 at 10:10

[GoogleCodeExporter]

This feature is inspired by a similar feature in the gnieh-pp library by Lucas 
Sabatin.

Original comment by inkytonik on 22 Jan 2013 at 10:15

[GoogleCodeExporter]

Original comment by inkytonik on 22 Jan 2013 at 10:15

• Changed state: Accepted

[GoogleCodeExporter]

We went around on this question a bit and couldn't really decide what 
pretty-printing truncation meant. In general, it might be necessary to 
pretty-print all of a structure in order to work out how many lines it has. 
Therefore, it's not clear what it would mean to truncate *during* 
pretty-printing.

For now we have settled on a simpler variant for which the meaning is clear. In 
rd91866d1017b, we have added filter functions in org.kiama.output.Filters which 
implement ways to filter the complete pretty-printer output. E.g., keepMaxChars 
and keepMaxLines keep the string within character count and line count limits. 
More interestingly, keepMaxIndent can be used to omit lines that are indented 
more than a certain amount, so the full string is summarised to a particular 
depth.

We considered building in a "run optional filter" aspect to the operation of 
the "pretty" method of pretty-printers, but it seemed easier to keep filters 
separate since their interfaces may well vary.

As experience illuminates, we will add more useful filters. E.g., it might be 
good to extend the character and line filters to take a lower-bound as well, so 
we could do thinks like pull a segment out of the middle.

Original comment by inkytonik on 19 Feb 2013 at 4:41

• Changed state: Resolved