Allow lint gutter hover time to be configured #4

Merged
hubgit merged 5 commits from lint-gutter-config into main 2022-02-25 12:31:30 +01:00
hubgit commented 2022-02-24 15:39:17 +01:00 (Migrated from github.com)

It would be useful to be able to configure the value used by the lintGutter extension for hover time (delay).

This adds a config parameter with boolean hoverTime property, defaulting to the existing constant Hover.Time.


A screen recording of a hover with hoverTime set to 1:

https://user-images.githubusercontent.com/14294/155545229-0c49202c-afce-45b8-8d92-b599849bfd42.mov

It would be useful to be able to configure the value used by the `lintGutter` extension for hover time (delay). This adds a `config` parameter with boolean `hoverTime` property, defaulting to the existing constant `Hover.Time`. --- A screen recording of a hover with `hoverTime` set to `1`: https://user-images.githubusercontent.com/14294/155545229-0c49202c-afce-45b8-8d92-b599849bfd42.mov
marijnh commented 2022-02-25 09:55:58 +01:00 (Migrated from github.com)

Do you really need that margin to be configurable?

Do you really need that margin to be configurable?
hubgit commented 2022-02-25 10:03:19 +01:00 (Migrated from github.com)

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.

> 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.
marijnh commented 2022-02-25 10:29:28 +01:00 (Migrated from github.com)

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 LintGutterConfig if 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).

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 `LintGutterConfig` if 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).
marijnh commented 2022-02-25 12:31:46 +01:00 (Migrated from github.com)

Thank you.

Thank you.
Sign in to join this conversation.
No reviewers
No labels
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
codemirror/lint!4
No description provided.