search

banacorn / agda-mode-vscode

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

Add "!editorHasSelection" condition to agda-mode.lookup-symbol #131

Closed jespercockx closed 1 year ago

jespercockx commented 1 year ago

All commands that start with Ctrl-C or Ctrl-X have the condition !editorHasSelection, except for this one:

https://github.com/banacorn/agda-mode-vscode/blob/905ec6189976b98f6806d73c735c9602c0f39bda/package.json#L767

This is annoying since it blocks Ctrl-X from being used for cutting text. Adding the condition fixes the problem.

jespercockx commented 1 year ago

Actually this is a duplicate of https://github.com/banacorn/agda-mode-vscode/issues/47