Hover delay for lint errors

We’re finding that the 600ms delay showing lint hovers is long enough that folks less familiar with code editor behaviour start trying other interactions with the red underline (e.g. right click). I think it would help if it was quicker to to raise.

Visual Studio Code’s equivalent timeout appears to be 300ms by default and is configurable.

Would you consider revisiting the default or adding configurability? For the moment I only care about lint errors, though this might apply to other tooltips too.

It looks like there’s low-level undocumented support for setting the timeout but I don’t think it’s exposed by packages like lint.

The patch below exposes this option and adjusts the default (whose initial value I just pulled out of thin air). There’s no obvious way to make this configurable from the lint extension without adding new moving parts, so for the time being I punted on that until someone explicitly needs it. Does this work for you?

That’s great, thank you.

Great, I’ve tagged @codemirror/tooltip 0.19.15