search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 40 forks source link

Ctrl-X doesn't work as cut with agda-mode #47

Open ice1000 opened 3 years ago

ice1000 commented 3 years ago

image

Please save me, I love cut and paste!

lacrosse commented 3 years ago

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

banacorn commented 3 years ago

@lacrosse Can you be more specific about the commands you are using with in the built-in terminal?

lacrosse commented 3 years ago

@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.

barrettj12 commented 2 years ago

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.

banacorn commented 2 years ago

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?

ice1000 commented 2 years ago

I also believe that it's vscode's fault

lunar-starlight commented 2 years ago

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.

James-Fraser-Jones commented 2 years ago

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-= ?

jespercockx commented 1 year ago

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.