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

Re #79: Disable activating input method inside the search box #155

Closed vic0103520 closed 1 year ago

vic0103520 commented 1 year ago

I adjust the condition of activating input method to enable inputting '\' into the search box.

vic0103520 commented 1 year ago

In addition, I think it's possible to have Unicode input in the search box if we separate activation in the text editor and the search box by adding a new command like "agda-mode.input-symbol[ActivateInFindWidget]".