feat: sticky notifications for extension startup errors #547
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
mhuisi
force-pushed
the
mhuisi/setup-diag-ux
branch
from
5da6bd0
to
ce7bb48
Compare
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 PR changes the notifications for extension startup errors to a new "sticky" notification mechanism.
Before this PR, when one of the precondition checks of the extension failed (e.g. because Lean was not installed), we would issue a small non-modal notification in the bottom right and then rely on users to figure out that after fixing their setup, they need to open a new Lean document to restart the check. If users closed this notification, there would also be no further indication for why the extension is not activating.
This is quite unintuitive, so we now instead issue a modal notification when the error first occurs and then a sticky notification that re-appears whenever a new Lean text editor is made visible. Clicking the retry button on this notification will re-try the check. This way, it's much harder to miss the error and how to restart the check.
Since these new sticky notifications invert the control flow, this PR required a broad refactoring of the notification architecture.
This PR also fixes a bug where starting VS Code on an untitled Lean 4 file would not start the language server and introduces a new Lean 4 specific abstraction layer for VS Code API event handlers. This abstraction layer is currently only in use in the code that had to be refactored for this PR, but it will be introduced more broadly in further PRs.