agda-mode-vscode
agda-mode-vscode copied to clipboard
banacorn
Ctrl-X doesn't work as cut with agda-mode
A subset of this issue is affecting me. I'm using agda-mode on a Mac so copy/paste isn't affected, but I need to use Ctrl+C, Ctrl+X, etc. in the built-in terminal. I fixed it locally by adding && editorTextFocus to every problematic shortcut's when clause, perhaps this should be added to the repo? @banacorn
@lacrosse Can you be more specific about the commands you are using with in the built-in terminal?
@lacrosse Can you be more specific about the commands you are using with in the built-in terminal?
Ctrl+C is frequently used in the terminal to abort the current process. I could be doing git push, say, and pressing Ctrl+C to abort it upon seeing git ask me the passphrase to the wrong private key. Ctrl+X is used to exit the nano editor, etc.
I'm still having this issue on Windows 10. C-c for copy seems to work when something is selected, but C-x always gives the message
(Ctrl+X) was pressed. Waiting for second key of chord.
even when text is selected.
VS Code's key binding resolution is pretty awful.
I'm not sure what can we do to mitigate that.
Perhaps moving C-x commands to somewhere else?
agda-mode.lookup-symbol doesn't have !editorHasSelection, which is what prevents the C-c chords from interfering with copy. If you just move that one it will fix cut.
This is also causing an issue for me. From looking at the bindings, it seems the culprit is:
{
"command": "agda-mode.lookup-symbol",
"key": "ctrl+x ctrl+=",
"when": "agdaMode && !terminalFocus"
}
which can't use !editorHasSelection for obvious reasons.
Perhaps that specific binding could be changed to something else like C-y C-= ?
which can't use !editorHasSelection for obvious reasons.
Why not? In Emacs this just gives the definition of the symbol at the current position of the cursor, so we could do the same in VS code.
