vscode-lean4
vscode-lean4 copied to clipboard
leanprover
InfoView font size
The font size (and family) is taken from the editor font by default. It will also change font size along with the rest of the UI when you press ctrl++ or ctrl+-. If you want more customization, then the lean4.infoViewStyle property allows you to style the infoview with arbitrary CSS.
Yes I found lean4.infoViewStyle, but how do you use it exactly? Exposing CSS like this is powerful, perhaps too powerful for normal users that have no idea what CSS is...
I was surprised that this setting did not affect it
and most other parts of vscode have their own explicit 'font size' properties.... (markdown preview, debug console, terminal, etc).
Yes I found lean4.infoViewStyle, but how do you use it exactly?
You can set it to body { font-size: 30px; } for example.
I was surprised that this setting did not affect it
Wait, the "Font Size" setting should have an effect. Ah, but only after you restart vscode, and then only for the code in the infoview (and not the other text)...
and most other parts of vscode have their own explicit 'font size' properties.... (markdown preview, debug console, terminal, etc).
I'm not against it, such a setting seems like a reasonable addition. (It would also be great if the changes were applied immediately and you didn't have reopen the infoview.) You're the first to ask for this feature though!
Marked as a low priority since none of the actual users asked for this feature.
Just a note to say I'm an actual user and I would love this feature!
