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

Published 20 hours ago • verified publisher icon banacorn

Dead keys

Open barrettj12 opened this issue 2 years ago • 4 comments

I have an issue that some of my keys/keybindings no longer work during/after using agda-mode:

  • \ (in search bar)
  • (
  • )
  • C-x
  • C-c

This doesn't happen every time, and not all of these will necessary happen at once. Generally, the only fix is to restart VSCode. I'm not sure what could be causing it.

barrettj12 avatar Nov 19 '21 16:11 barrettj12

Does this happen in Agda files, or/and files other than Agda?

banacorn avatar Nov 24 '21 05:11 banacorn

I think only Agda files - I haven't noticed it in other files.

barrettj12 avatar Nov 24 '21 09:11 barrettj12

I'm on Mac, and I've noticed that C-x C-c initially doesn't work. C-x is silently ignored, and I get this message:

C-c was pressed. Waiting for second key of chord...

Once I run "Agda: Load" (C-c C-l), the C-x C-c combo starts working fine.

joliss avatar Nov 30 '21 19:11 joliss

Once Agda is loaded, I'll also sporadically get this error:

The key combination C-x C-c is not a command

Simply retrying the C-x C-c combination a few times usually makes it work.

joliss avatar Nov 30 '21 20:11 joliss