Disabling proof-unicode mode does not disable Unicode shortcuts

[Ptival]

When Coq starts up, typing -> inserts -> and displays →.

But from the moment a single proof-unicode-toggle command is issued, typing -> will always insert → (and of course, always display →), no matter how many time you toggle.

My expectation was that toggling twice would not only revert the display, but also revert the input. Otherwise, there should be an orthogonal, documented way of turning off the input replacement feature.

Thanks!

[cpitclaudel]

Hmm, proof-unicode-tokens-toggle works for me, and I don't have a proof-unicode-toggle command. Try turning off company-coq, if you use it? It can make it trickier to know whether symbols are actually being inserted or just displayed.

[Ptival]

Yes, sorry, I meant proof-unicode-tokens-toggle. To reproduce my problem, the following steps:

• Run emacs w/ proofgeneral with some .v file.
• Run company-mode (Company mode disabled in this buffer).
• Type a -> b, it shows as a → b (for me at least).
• Run proof-unicode-tokens-toggle
• Type a -> b, it also shows as a → b, though the arrow is slightly different.
• Run proof-unicode-tokens-toggle, now the first one looks like a -> b, but the recent one looks like a → b
• There is no longer any way to enter -> by typing ->. You can confirm it is the case by saving the file and opening it in a different editor. From now on, typing -> will always produce the character →, no matter if you toggle Unicode tokens.

[cpitclaudel]

You want company-coq-mode, not company-mode, I think

[cpitclaudel]

This is what I get if I run your experiment : a -> b a → b a -> b. I wonder if I'm doing something wrong.

[hexchain]

I thought I had encountered this issue with PG and company-coq. In my case, after starting Emacs:

1. In PG "unicode tokens" is disabled, while company-coq's "prettify symbols" is enabled.
2. Executing proof-unicode-tokens-toggle actually enabled that setting but nothing visible is changed in the buffer, because of company-coq.
3. Executing proof-unicode-tokens-toggle again should disable that setting and the buffer should have its original content, but "prettify symbols" is still enabled. Also, I'm not sure why in this state the "Unicode tokens" input method is still functioning, that's probably the reason why inputting -> still turns into →.

[cpitclaudel]

To be clear, proof-unicode-tokens isn't really maintained anymore