The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Benjamin and Michael,

On 02/26/2016 09:34 AM, Benjamin C. Pierce wrote:
>  1. I wonder whether beginning users will find the available input methods 
> confusing or off-putting 

On 02/26/2016 12:32 PM, Soegtrop, Michael wrote:
> 1.) Using Unicode notations in the HTML version but ASCII in the IDE is as 
> confusing as finding the shortcuts for the right symbols [...]
> 3.) The shortcuts for the Unicode symbols can be mentioned in IDE menus at 
> a prominent place

As an experiment, I've added input and prettification hints to company-coq. 
When the point is on a prettified symbol (such as ‘fun’ being displayed as 
‘λ’, or ‘nat’ being displayed as ‘ℕ’), company-coq now shows a message 
similar to these:

  ‘λ’ is a prettified version of ‘fun’.
  ‘ℕ’ is a prettified version of ‘nat’.

On the other hand, when the point is on a Unicode symbol, such as ‘∪’ or ‘⊕’, 
company-coq now shows a message similar to these:

  To input ‘∪’, type ‘\cup RET’.
  To input ‘⊕’, type ‘\oplus RET’.

There are screenshots at 
https://github.com/cpitclaudel/company-coq/#misc-extensions-of-proof-general

As always, comments and suggestions are very welcome! Let me know what you 
think.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature