(VS code extension) `:hover` for CSS classes?

Stream: lean4

[Thomas Murrills]

In std4#215, Try these:, I'm considering trying to allow the widget implementer to choose simple Lean-based styles for clickable suggestions. For example, if we're suggesting hypotheses, we might want to style each suggestion according to .goal-hyp, or if the suggestion produces an error, we might want to style it according to the appropriate .error style (note that the LLMStep project wants to style unparsable suggestions as error-like, so this isn't an imagined use case).

The issue is that when hovering over the suggested text, the a:hover class (from VS code) takes precedence, and the text flashes to blue.

I can hack my way around this if I need to by dynamically altering the CSS via javascript to include e.g. .error:hover or a.error:hover. But I was wondering if there'd be interest in adding these :hover styles to the CSS in the extension, since this is pretty easy to do—or if there's a different way this minor issue should be dealt with. :)