Agda Mode Keyboard Shortcuts does not Work Except Loading a File

[Naruyoko]

Steps to Reproduce

1. Open a file
2. Load the file using Ctrl + C Ctrl + L
3. Attempt running an Agda mode command through a keyboard shortcut, e.g. Agda: Quit via Ctrl + C Ctrl + Q

Expected behavior: The file is loaded, then the Agda mode command is executed.

Actual behavior: The file is loaded, but the Agda mode command is not executed ("The key combination is not a command."). With keyboard shortcuts console output, I see From 42 keybinding entries, matched chord, when: editorTextFocus && !editorHasSelection && editorLangId == 'agda', source: user extension banacorn.agda-mode. on Ctrl + C but From 1 keybinding entries, no when clauses matched the context. on Ctrl + Q.

Additional Information

I got this issue when I updated VS Code to 1.74.1. It worked and continues to work on 1.69.2. I am using Windows 10 and x64 .zip downloads of VS Code.

[Naruyoko]

With further testing, it works with 1.73.1 but fails with 1.74.0.

[makotokanazawa]

I'm experiencing the same issue with macOS Monterey 12.6.2 (both on Intel and Apple Silicon).

[9Y0]

I'm also experiencing this with Linux Mint Mate 20.3, VS Code 1.74.1

[eeoam]

I am also experiencing this problem on Ubuntu 22.04.01, VSCodium Version: 1.74.1

[eduardz1]

experiencing the same issue, running the commands with CTRL-Shift-P works, "Agda: Case" shows no preview of what's being written but still works.

Windows 11 VSCode 1.74.2 Agda 2.6.2.2

[hyc3z]

ctrl+shift+P to show Agda command, click the gear, right click and select "Change When Expression"

and change to editorTextFocus && !editorHasSelection && editorLangId == 'agda'

worked for me for C-c C-c and C-c C-Space, not tested on other commands.

[mjaskelioff]

The problem seems to be the agdaMode condition in the shortcuts being detected as False. Changing it to the editorLangId == 'agda' seems to fix it.

[Anrock]

My observation is that agda shortcuts tend to work if file type is plain text and stop working when you set it to agda. But there is a semi-reliable workaround I've found to have both shortcuts working and have highlights without editing shortcuts.

1. Open agda file
2. Make sure that file type is set to Agda
3. C c C l, wait for load
4. Use Agda: Quit and Restart from Ctrl+Shift+P

Probably there is also a requirement to keep text cursor inside a hole but I'm not sure.

[mrshiposha]

My observation is that agda shortcuts tend to work if file type is plain text and stop working when you set it to agda. But there is a semi-reliable workaround I've found to have both shortcuts working and have highlights without editing shortcuts.

1. Open agda file
2. Make sure that file type is set to Agda
3. C c C l, wait for load
4. Use Agda: Quit and Restart from Ctrl+Shift+P

Probably there is also a requirement to keep text cursor inside a hole but I'm not sure.

I've taken these steps and now all the combinations work fine. I did not hold the cursor inside a hole.

Thanks!

[Steven1677]

I've solved this issue using [hyc3z](https://github.com/hyc3z)'s solution.

Although I don't know what is really happening to VSCode's update, which breaks the agdaMode context trigger, I've tried to modify package.json by replacing every agdaMode with editorLangId == agda in the keybinding section. It seems that this rough fix works.

[berndlosert]

I also have this issue and solved it by changing the commands to use editorLangId == 'agda'. Someone already made a PR to fix the problem. Could we get it merged?