The Coq mailing list

[Clément Pit--Claudel <clement.pit 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.

That's definitely an issue. It tends to be less of a problem in practice than 
I expected, though; maybe because I tend to align things as

  forall x y,
    x + y.

instead of the style above. We can also teach Emacs to ignore prettifications 
for indentation purposes.

Another, related issue is uncommon characters not being available in your 
monospace font, and thus breaking alignment (ever so slightly). It makes 
block editing a pain. My attempt at fixing that is at 
https://github.com/cpitclaudel/monospacifier.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature