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

Fix issue #76: Input method is reactivated after entering a backslash… #154

Closed vic0103520 closed 1 year ago

vic0103520 commented 1 year ago

When input method is activated, entering a backslash will reactivate input method. If the buffer is empty, it will insert a backslash into the editor instead.

banacorn commented 1 year ago

Thank you