CODEWITHSUNDEEP
visual-studio-codekeyboard-shortcutsagdavscode-keybindingagda-mode
glvcsygrg
glvcsygrg

Reputation: 1

"command 'agda-mode.input-symbol[BrowseLeft]' not found" error in VSCode everytime I try to browse now with arrow keys

I have no idea what happened. I was doing some Agda work in one window, and I had a C project in another. Restarted VS Code to work on the C project, now every time I try to use arrow keys I get the error message mentioned in the title, and my cursor won't move.

I looked at my Keyboard shortcuts and found this:
List of keyboard shortcuts concerning arrow keys and agda-mode

Disabling the extension and restarting didn't work.

Upvotes: 0

Views: 102

Answers (1)

starball
starball

Reputation: 50385

I'm not sure why this happened (either), but somehow your extension-scoped settings got copied over to your user-scoped keybindings config file, and they got copied over without copying over the when clauses, so they're applying at all times, in all contexts (that's why disabling the extension and restarting didn't work: the copied keybindings in your user-scoped keybindings were still active, and were then pointing to commands defined by a disabled extension).

To fix the issue right now, you should delete those copied-over keybindings from your keybindings config file (Preferences: Open Keyboard Shortcuts (JSON) in the command palette).

Upvotes: 0

Related Questions