The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Note that with Coq, one can use Unicode notations (saved in the file thus, and not just displayed as pretty symbol). For inputting Unicode characters, Company-Coq provides a special feature: type the latex name, starting with \ and then Ctrl+Enter.

Le mar. 7 mars 2017 à 14:57, Christian Doczkal <christian.doczkal AT ens-lyon.fr> a écrit :

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.
>