Open nkaretnikov opened 7 months ago
The technical limitations part refers to the upstream issue in VSCode, which I believe has been implemented: https://github.com/microsoft/vscode/pull/175253.
Great news!
Personally, I would like to use the Emacs shortcuts as the default. But I'm thinking maybe we can also keep both shortcuts (Emacs + current), it's that's not too pollutive.
I haven't tested this, but based on the README:
The technical limitations part refers to the upstream issue in VSCode, which I believe has been implemented: https://github.com/microsoft/vscode/pull/175253.
If so, the default shortcuts need to be changed to match Emacs because that's the current go-to editor for Agda, which many users will be familiar with. Emacs shortcuts are also something you can see often in third-party documentation or tutorials, just because it's the default. By having the same set of shortcuts, it'll make it easier for current Emacs users to transition to this extension.
As an aside, I personally prefer more ergonomic shortcuts, like in Spacemacs, but that can always be configured by the users. This can be also provided in settings, in addition to the default Emacs shortcuts.
I think there's also value in keeping the current shortcuts as is because they are more ergonomic than the default Emacs ones. So this could be a setting in the configuration: