InfoView focus issue

Stream: lean4

[Marc Huisinga]

Since VS Code 1.88, there has been an issue where right clicking almost anywhere in VS Code will focus the InfoView. This means that e.g. right clicking and clicking "Go to Definition" will open documents in the tab group of the InfoView, not that of the text editor.

Since this occurs for all webviews and is only dependent on the VS Code version, not the vscode-lean4 version, this is most likely a VS Code bug. I've reported it here: https://github.com/microsoft/vscode/issues/212679

If you want to see this issue fixed, upvoting the issue probably doesn't hurt.

[Damiano Testa]

Thanks! I noticed this and was not sure whether to report it or not, but it is quite annoying.

[Kim Morrison]

@Kyle Miller has pointed out that that you can click the "..." icon in the top right of the infoview, and select "lock group", and that this solves some of these problems.

[Marc Huisinga]

For another workaround, it turns out that you can manually edit your settings.json file to always auto-lock the InfoView, despite the fact that VS Code provides no UI for this.

Open your settings.json via Ctrl+Shift+P > Preferences: Open User Settings (JSON). Then, copy and paste the following entry and ensure that the resulting JSON is correct (e.g. inserting trailing commas):

"workbench.editor.autoLockGroups": {
  "default": false,
  "workbench.editor.chatSession": false,
  "workbench.editorinputs.searchEditorInput": false,
  "workbench.editors.gettingStartedInput": false,
  "terminalEditor": true,
  "jupyter-notebook": false,
  "imagePreview.previewEditor": false,
  "vscode.audioPreview": false,
  "vscode.videoPreview": false,
  "jsProfileVisualizer.cpuprofile.table": false,
  "jsProfileVisualizer.heapprofile.table": false,
  "jsProfileVisualizer.heapsnapshot.table": false,
  "workbench.input.interactive": false,
  "mainThreadWebview-markdown.preview": false,
  "mainThreadWebview-simpleBrowser.view": true,
  "mainThreadWebview-browserPreview": true,
  "mainThreadWebview-lean4_infoview": true
}

This is the default autoLockGroups setting with an extra entry that auto-locks the InfoView. VS Code will produce a warning because you're really not supposed to add any additional entries here, but we can ignore that and it will still work. Finally, restart VS Code, open a Lean document and observe that the InfoView is now locked.

I haven't tried it yet, but it may be possible to add this setting to a VS Code workspace settings file, too.

We unfortunately can't do this automatically in the VS Code extension because of https://github.com/microsoft/vscode/issues/185674.

[Marc Huisinga]

It looks like on the most recent VS Code versions, this issue has been resolved upstream.