agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

Deactivation of *latex-input*?

Open MevenBertrand opened this issue 3 months ago • 0 comments

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?

MevenBertrand avatar Mar 25 '24 18:03 MevenBertrand