search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

Deactivation of *latex-input*? #184

Closed MevenBertrand closed 3 days ago

MevenBertrand commented 5 months ago

I use the latex-input plugin to provide access to unicode characters. I've grown used to this, which I use across all languages in VSCode, and so I'd like to keep using it instead of Agda's home-grown input method. However, it seems like there is some sort of conflict happening: in all other 5 or 6 language mode I quickly tried, typing \ in opens up an auto-complete pop-up, as expected, see this screenshot: Screenshot from 2024-03-25 18-26-11 However, turning on the agda-mode plugin (or changing the language of the file to Agda) seems to break that. Do you know what might be causing this, and how I could fix it?

banacorn commented 3 days ago

Please try disabling the input method of agda-mode and check if there are still any conflicts under Agda Mode › Input Method.

MevenBertrand commented 2 days ago

I have tried disabling the input method, but it does not seem to have any effect on my issue. I also tried changing the input method activation key, and brutally removing the keybinding from the keybindings list, but this does not help either.