Goals don't update on cursor movement when using VsCodeVim

[jesyspa]

As discussed on Zulip, in version 0.1.2 of coq-lsp, when show_goals_on is set to "Show on click and cursor movement" and the VsCodeVim extension is enabled, moving the cursor using hjkl or the arrow keys doesn't update the goal status (and in fact there's no activity in Coq LSP Server Events).

[ejgallego]

Indeed, it seems that the problem is that VsCodeVim doesn't call window.onDidChangeTextEditorSelection which is what coq-lsp uses to keep track of the cursor.

@jesyspa maybe we could ask the VsCodeVim developers what's the correct way to track cursor movement when their extension is enabled?

I bet they use their own selection implementation which indeed makes sense for something like a VIM emulator.

This way, we could detect that and hook to the correct method.

[jesyspa]

I don't have any experience with writing VS Code plugins so I may be misunderstanding: should it be on each plugin to notify when the text editor selection changes, or is this a VSCode issue? I tested it with vscode-neovim and the behaviour is the same...

It seems like for normal movement, VsCodeVim uses the cursorMove built-in command, though I may be misreading it. I can't find anything in the documentation about whether cursorMove should call onDidChangeTextEditorSelection (or anything else). I'm looking to see whether there's any good way to get a log of all raised events to see what gets triggered...

[jesyspa]

A little bit of testing later: the events are being generated, but they have type Command instead of type Keyboard, hence why they're being ignored. I'm not sure why this would be the case: I can't see anything in the options of cursorMove that would determine one or the other...

I think the simplest solution may be to add a corresponding option for show_goals_on, or treat Command as Keyboard. What do you think?

Here's the code of the extension I cooked up to test this: https://github.com/jesyspa/jytest-vscode

[ejgallego]

Oh, that's a great finding @jesyspa , I think indeed with that info we can fix your problem.

Indeed I wonder if there is a problem in identifying Command with Keyboard, not sure if some extensions can use that programatically and hence create a bit of chaos in terms of goal display, let's have a look at the docs.