fix: broken document symbols

[mhuisi]

This PR fixes an issue reported at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/VSCODE.20outline.20mode.20not.20working.20in.20imports/near/442000461 that caused the VS Code outline and other features that rely on document symbols to not display anything when initially opening the document.

The synopsis is as follows (in case anyone stumbles upon related issues in the future):

1. By default, VS Code triggers onDidOpenTextDocument when hovering over an identifier while holding Ctrl, which in turn makes the language client library emit a didOpen notification to the language server (closely followed by didClose when moving the mouse away from the identifier).
2. This puts unnecessary pressure on the language server since it starts elaborating the file, especially given that VS Code does not emit any further requests in this situation.
   Ctrl+hover (goto definition preview) causes textDocument/didOpen(/didClose) events microsoft/vscode#78453
   VSCode extension runs into infinite leanpkg spawning loop on Ctrl+hover lean4#367
3. Hence, it was suggested to filter these notifications in the language client middleware by only sending these notifications for window.visibleTextEditors, which does not contain "synthetic" documents like the one opened in the Ctrl hover.
4. This doesn't work because window.visibleTextEditors is not up-to-date yet when the corresponding onDidOpenTextDocument handler is executed.
5. To work around this, Only send didOpen for visible text documents. #17 filtered all didOpen notifications emitted by the client and registered its own handler to emit these notifications. This handler was executed after window.visibleTextEditors had been updated and so could use window.visibleTextEditors to decide for which files didOpen should be emitted. See Add options to only sync visible documents to the server microsoft/vscode-languageserver-node#848 for the currently still open issue to properly fix this in the language client library.
6. This worked fine until we added language server support for requests that are commonly emitted right after the file is opened (e.g. document symbols).
7. Since the language client registers its own handlers for emitting requests and vscode-lean4 manages didOpen notifications, there's now the potential for a race condition: If the handlers from different sources are called in the wrong order and a file is opened after a request is emitted, the language server may respond to the request with an error since it doesn't know about the document yet.
8. VS Code does not frequently issue these requests if the file doesn't change, so the empty state sticks around until the document is changed (or even longer for some requests).
9. This causes an empty document symbols view when initially opening the document, which is especially critical when using 'Go to Definition'.

In VS Code version 1.67 (long after the initial vscode-lean4 work-around for this issue), a new window.tabGroups API was added that allows querying all documents that are currently open in VS Code tabs. window.tabGroups is fortunately already up-to-date when onDidOpenTextDocument is called, so we can now use this information to directly filter the didOpen notifications in the language client middleware without registering our own handler that introduces a race condition. This fixes the bug.

One strange thing I noticed while debugging this issue is that VS Code actually emits multiple requests of the same kind when the document is first opened. One of these typically fails because the document is not open yet whereas the second one typically succeeds. But for some reason (I suspect a bug), VS Code does not actually end up using the result of the successful request in this case. This lead to a very confusing situation during debugging where both the language server and the language client library seemed to return a correct result, but VS Code still produced an empty outline.

I also suspect that this issue is one cause of other non-deterministic issues that we have previously encountered in the language server. For example, while we already fixed this issue using other means, the non-deterministic behavior of semantic highlighting sometimes being broken (leanprover/lean4#2977) may also have been partially caused by this as VS Code queries the semantic tokens for the full document right after opening the document as well and only rarely re-queries them afterwards.

This PR also replaces our own tracking of documents opened in the language server with the open documents tracked by the language client library. I suspect that the language client library has a bug here (the set of openDocuments in the language client library will probably also contain documents that were filtered in the didOpen middleware if the document was opened while starting the client), but it shouldn't affect us as we only filter didOpen notifications for documents that can only be opened after the language client was already launched.