Fixes stuck hover widget when triggered manually, with "editor.hover": false#52147
Merged
alexdima merged 1 commit intomicrosoft:masterfrom Jun 25, 2018
Conversation
"editor.hover": false745a1e2 to
f26117c
Compare
ef519ae to
dbcb672
Compare
- Adds support to toggle hover without reloading the editor
dbcb672 to
605ba83
Compare
Contributor
Author
|
This PR was in conflict after the commit from @alexandrudima on June 22nd, but I've addressed the conflicts and its merging cleanly again. @alexandrudima / @rebornix could you please review and let me know if there's any value in merging or any other feedback? Thanks! |
Member
|
👍 Thank you! |
This file contains hidden or 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
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
If the editor's preference
editor.hoveris set tofalseand the hover widget is triggered withCMD + K,CMD + I, it gets stuck in the page and does not go away with interactions such as mouse movement, mouse leave, editor scroll or editor model changes. This PR fixes this behaviour by hiding the tooltip when the above interactions happen.Also, this PR adds support to react to changes on the preference
editor.hoverwithout having to reload the editor, effectively allowing the plugin suggested by @rebornix to work for the use case of #25715.