Zulip Chat Archive

Stream: lean4

Topic: Infoview style

Patrick Massot (Sep 27 2023 at 15:33):

Does anyone know how to actually use the VSCode extension setting Lean4: Infoview:Style? I can't get anything out of it. I know I can open developer tools and find the CSS class I want to modify, but it doesn't seem to work.

Alex J. Best (Sep 27 2023 at 15:35):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Infoview.20colors/near/386854615 worked for me (at the time)

Alex J. Best (Sep 27 2023 at 15:35):

Maybe you are missing important!

Alex J. Best (Sep 27 2023 at 15:36):

I think due to the order the styles are loaded in or something this is needed for things to actually have an effect

Patrick Massot (Sep 27 2023 at 17:03):

Actually that was me not remembering how CSS works. I'm sorry about the noise.

Last updated: Dec 20 2023 at 11:08 UTC