VSCode colors in Infoview

Stream: general

[Antoine Chambert-Loir]

Since a recent update of VSCode, the colors don't work well in the infoview window. For example, the hover-windows have no background which makes their content rather illegible when there is something beneath (and there often is). Everything is restored if I reload VSCode's Color theme, but I need to do all the time…

[Martin Dvořák]

FYI, I use this color settings:
https://github.com/madvorak/vscode-lean4-colors
It probably doesn't address your issue, but you can have a look at how both code appearance and infoview appearance are specified.

[Antoine Chambert-Loir]

thanks!

[Marc Huisinga]

Did someone else experience this issue? Did it persist?