InfoView stops updating afer "Lean 4: Resstart Server" command about vscode-lean4

[gebner]

Alex Bentkamp has reported a similar issue on zulip:

Any ideas where this message could come from?

Cannot send message to unknown document 'file:///home/alex/Projects/verified-optimization/code/DCP/DCP/Syntax/ProblemMacroMData.lean':
{"params":{"uri":"file:///home/alex/Projects/verified-optimization/code/DCP/DCP/Syntax/ProblemMacroMData.lean","sessionId":"7188571717961512369"},"method":"$/lean/rpc/keepAlive","jsonrpc":"2.0"}

I am on lean4:nightly-2021-10-18, VSCode, Ubuntu. These messages pop up constantly in VSCode's "Output" panel.

[lovettchris]

Interesting, I wonder if my fix to await webviewPanel.api.initialize in my PR helps with this at all...

[Vtec234]

Looks like this has been fixed in our recent changes. If anyone is still observing the issue, please reopen.

[lovettchris]

Agreed