Custom hovers in VSCode

Stream: lean4

[Trebor Huang]

Is it possible or planned to let the user be able to customize hover messages, or other places where the display is richer than just text? For instance, someone working with colors could potentially benefit from being able to preview the color either by hovering or elsewhere in VSCode.

I understand that this may be difficult to implement in other places, but presumably having a fallback wouldn't hurt.

[Sebastian Ullrich]

Have you seen https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/by.20interactive!/near/310860373?