leanprover
Stale dependency diagnostic does not show up under 'Messages' after opening VS Code
Description
Typically, when opening a file with a stale dependency, there is a diagnostic under 'Messages' that informs us that 'Restart File' needs to be called. However, right after VS Code is opened and the extension launches for the first time, that diagnostic only appears in the editor and under 'All Messages' after unfolding the section, not in 'Messages'. It would be nice if this was fixed so the error is always visible in the InfoView.
Additional Information
I suspect that this is due to a race condition caused by how the InfoView is informed about new diagnostics; when the stale dependency diagnostic is received, the InfoView probably isn't listening for these diagnostics yet.
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
