The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello,

I also use the Company-Coq prettify-symbols method. The main reason for
me is that this is "safe" in the sense that no actual unicode characters
are written to the file.

I haven't experimented with the "Unicode Tokens" feature for a while,
but a quick test confirms that his method (sometimes) generates actual
unicode symbols (i.e., in my case -> is saved as unicode arrow while
forall is not). I faintly recall that I had trouble with coqdoc/browsers
to reliably get the unicode symbols to work.

So I guess this touches on the issue whether unicode symbols should be
"display only" or actual characters. I see advantages and disadvantages
for either so I'd say that for the time being both should stay around.

Best,
Christian


On 06/03/17 21:47, Clément Pit-Claudel wrote:
> On 2017-03-06 15:29, Théo Zimmermann wrote:
>> That's another feature which is also provided by Company-Coq  (advertised 
>> as prettification), right?
> 
> Correct.  A bit less general, but based on Emacs primitives instead of 
> custom fontification rules.
>