Only send didOpen for visible text documents. #17
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
1 task
mhuisi
added a commit
that referenced
this pull request
Jun 4, 2024
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. microsoft/vscode#78453 leanprover/lean4#367 3. Hence, [it was suggested](microsoft/vscode#78453 (comment)) 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, #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 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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
THIS BREAKS THE LEAN 3 EXTENSION (probably).