Server does not respond to new file

[b-mehta]

Description

The lean4 server does not display any information or errors on a new file.

Context

Discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Server.20crashes.20on.20new.20file

Steps to Reproduce

1. Have a running Lean server, working on a Lean file
2. Open a new file in VSCode in the same directory
3. Save it as test.lean
4. Write example : 1 = 2 := rfl in the file
5. Save the file
6. No errors are generated.

Expected behavior:
The invalid theorem gives an error.

Actual behavior:
The invalid theorem does not give an error.

Versions

vscode-lean4 version: 0.0.168
Lean version: 4.9.0-rc2
OS version: MacOS Monterey

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[b-mehta]

Recording the workaround from the zulip thread for anyone coming across this:

You can close test.lean and then re-open it. Then, when the language client attempts to open the document, VS Code will already have updated window.tabGroups.