The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/11/2016 10:22 AM, Pierre Courtieu wrote:
> Hi,
>
> Concerning prettification there is one problem that is difficult to solve:
> indentation. Look for example at the following code that is indented for
> non-prettified display:
>
> forall x y, x +
>              y.
>
> This will not look good if prettified:
>
> ∀ x y, x +
>              y.
>
> And conversely a good indentation in prettified mode would not look good in
> non prettified.
>
> In pg+company-coq indentation is done according to the current mode
> (prettified or not), but user opening the file with the other mode will
> have ugly indentation.
>
> P.

A similar issue occurs with splitting lines to prevent wrapping.  A line 
with many prettified (hence shortened) symbols can be split much later 
when prettified than it would need to when not to keep from wrapping.

Consider also prettification vs. Set Printing Width.  Currently, 
Company-Coq has an automatic Set Printing Width mode (the default, I 
believe) that tracks the buffer width.  However, it can't accommodate 
its own prettifications - unless it somehow takes over the line 
splitting chore from Coq.

I only noticed this when using Company-Coq to fold true and false to 
script/bold t and f, hence having many prettifications in the same 
term.  This enhances readability of terms where the bool constants occur 
often.  But when printed, the often severe shortening of the resulting 
lines makes for uneven output due to the splits occurring too soon.

-- Jonathan