Allow lint gutter hover time to be configured #4
Loading…
Add table
Add a link
Reference in a new issue
No description provided.
Delete branch "lint-gutter-config"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
It would be useful to be able to configure the value used by the
lintGutterextension for hover time (delay).This adds a
configparameter with booleanhoverTimeproperty, defaulting to the existing constantHover.Time.A screen recording of a hover with
hoverTimeset to1:https://user-images.githubusercontent.com/14294/155545229-0c49202c-afce-45b8-8d92-b599849bfd42.mov
Do you really need that margin to be configurable?
No, it was just sitting alongside the other constant so I thought it might as well be configurable. If reading the value from the state slows things down or has some other undesirable effect I'm happy to remove it from the config.
It should be pretty cheap, but I prefer not to put stuff in the public interface unless there's a known use for them, since once they are in there they have to stay around forever.
There's no need to export
LintGutterConfigif it's only used in a single place in the public interface.Also, please use my indentation style for long import lists (line-wrapped, with multiple on the same line).
Thank you.