Right-clicking almost anywhere in the editor makes "Lean Infoview" focused

[ge9]

Description

When I right-click somewhere unrelated to "Lean InfoView", the "Lean InfoView" tab is focused. Especially, when I right-click a lean source file and choose "go to definition", the file including the definition opens at the same pane as "Lean InfoView", which is undesirable. This also occurs when I right-click some other places like side bar or title bar or file explorer.

Context

This bug happen in VS Code 1.88 (March 2024) and 1.89 (Insider) but not in previous versions. I also tried vscode-lean4 released several months before, and this still happens. Therefore, this may be a bug with VS Code itself. But I don't see behavior like this in other situations (extensions).

Steps to Reproduce

1. Open some lean file and turn on Lean InfoView in a separate pane, as usual
2. Bring focus on the lean file, not InfoView
3. Right click somewhere (in lean file window or other place)
4. The focus moves to InfoView

Expected behavior:

The focus doesn't move

Versions

[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)]
109, 140, 143 [OS version] I reproduced this in Windows and Linux

[mhuisi]

I can reproduce this as well.