You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
Open some lean file and turn on Lean InfoView in a separate pane, as usual
Bring focus on the lean file, not InfoView
Right click somewhere (in lean file window or other place)
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
The text was updated successfully, but these errors were encountered:
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
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
The text was updated successfully, but these errors were encountered: