keep focus in editor after clicking [apply]

Stream: Editors & UIs

[Malvin Gattinger]

(This is actually about VSC, no other editor or UI. Hope the channel is okay for that too :wink:)

After accepting a suggestion from exact? or apply? by clicking on it in the InfoView I often want to continute typing. But I then need to (move the mouse coursor and) make a second click into the editor. Is there a way to keep the typing focus in the editor, so that immediately after accepting something by clicking [apply] I can type? (Or is it supposed to happen and did I mess up local settings?)

Somewhat related, as an alternative solution, I vaguely remember using a keyboard shortcut to accept a (the first) suggestion. What is it?

[Snir Broshi]

Ctrl+1 (or Cmd+1 on macOS) to focus back on the editor

[Snir Broshi]

Ctrl+. (or Cmd+.) to accept the suggestion without the mouse

[Malvin Gattinger]

Thanks, I think the emacs-like-keybinding extension I use messed up these standard shortcuts, will try to get them working again.

And I am still curious if the focus-change-effect of clicking can be prevented.

[Marc Huisinga]

And I am still curious if the focus-change-effect of clicking can be prevented.

Not to my knowledge. Note that there are cases where you do want clicking to focus the InfoView - e.g. when using the built-in trace search or the webview search (Ctrl+F).

[Mirek Olšák]

The extension could just return focus to the editor upon any edit, I tried it here
https://github.com/leanprover/vscode-lean4/compare/master...mirefek:vscode-lean4:insert-focus
It seems like at least for the case of text insertion, it was already an intention (maybe working, I haven't realized first that [apply] is an edit and not an insertion). What is an example infoview action to insert code to test this?

(disclaimer: I am no expert in the VSCode extension code, just experimented with it a bit using AI tools)

[Snir Broshi]

Mirek Olšák said:

What is an example infoview action to insert code to test this?

theorem foo : True := by simp?

[Mirek Olšák]

I think this is also an edit rather than pure insertion -- it must delete the ?. Perhaps I just don't understand what the handleInsertText is doing...

[Marc Huisinga]

Here's a quick implementation of Mirek's idea (refocusing the editor): vscode-lean4#702

[Marc Huisinga]

Mirek Olšák said:

I think this is also an edit rather than pure insertion -- it must delete the ?. Perhaps I just don't understand what the handleInsertText is doing...

I wouldn't stare too closely at that file, it's one of the only remaining ones from the before times and a lot of it doesn't make much sense ... :-)

[Mirek Olšák]

Marc Huisinga said:

Here's a quick implementation of Mirek's idea (refocusing the editor): vscode-lean4#702

How does that code differ from

await commands.executeCommand('workbench.action.focusActiveEditorGroup')

suggested by Claude? I suppose yours is more low-level?

[Marc Huisinga]

The difference is that it actually works, as opposed to that line suggested by Claude :-)

workbench.action.focusActiveEditorGroup focuses the currently active editor group (VS Code slang for "group of tabs in one specific panel"), e.g. when you focus something that isn't an editor, like a sidebar entry. When you focus the InfoView, that becomes the currently active editor group.

[Snir Broshi]

Mirek Olšák said:

await commands.executeCommand('workbench.action.focusActiveEditorGroup')

FWIW you could have tried it manually in VSCode by opening the command palette (Ctrl+Shift+P) and pasting the command ID workbench.action.focusActiveEditorGroup and selecting the first option

[Mirek Olšák]

I am a bit confused, are you suggesting it doesn't work at all? Of course I tried it before posting.

[Snir Broshi]

I tried it and it does not work, as Marc mentioned

[Snir Broshi]

(tried manually, not inside the extension)

[Mirek Olšák]

I used the extension debug -- Ctrl-F5 in the extension codebase.

[Marc Huisinga]

Mirek Olšák said:

I am a bit confused, are you suggesting it doesn't work at all? Of course I tried it before posting.

That code has a race condition. It doesn't work at all if you first focus the InfoView and then click the button, and it often works (but sometimes doesn't work) if clicking the button is what focuses the InfoView. Probably has something to do with the point in time at which VS Code decides to actually focus the InfoView when you click the button - there are multiple concurrent and communicating VS Code processes involved here, after all.

In general, I don't think that vibe-coding against the VS Code API is a good idea. There are lots of complicated subtleties that aren't documented anywhere.

[Mirek Olšák]

Thanks for the explanation. That makes sense, I tried only the direct click into infoview without focusing it before,
I am now experimenting with vibe coding a bit, especially on codebases I have no experience with. Sorry for annoying you with it.
On the other hand, the difficulties for vibe coding sound like difficulties for any potential newcomer.