Closing InfoView shows "Cannot read properties of undefined (reading 'api')"

[samuela]

Description

Closing the Lean InfoView shows a warning dialog with:

Cannot read properties of undefined (reading 'api')

This seems to happen when the InfoView pane is closed, not during normal editing.

Steps to reproduce

1. Open a Lean file in VS Code.
2. Make sure the Lean InfoView is open and active.
3. Close the InfoView pane.
4. Observe the warning dialog.

Expected behavior

Closing the InfoView should dispose of it cleanly, with no warning or error dialog.

Actual behavior

A warning dialog appears with the message above

Environment

• VS Code: 1.111.0
• Lean 4 VS Code extension: leanprover.lean4-0.0.229
• Lean toolchain: leanprover/lean4:v4.29.0-rc2
• Lean version: Lean (version 4.29.0-rc2, x86_64-unknown-linux-gnu, commit 83e54b65b65d1d3ce31d99d820a7bd5f3e219295, Release)
• Setup: VS Code Server / remote session

[mhuisi]

I couldn't reproduce this myself, but #756 fixes one potential cause of this issue. It has been released as part of the 0.0.232 pre-release. Could you try the pre-release and see if the issue still occurs?