search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
152 stars 45 forks source link

InfoView font size #40

Open lovettchris opened 2 years ago

lovettchris commented 2 years ago

how can the user customize the InfoView font size?

gebner commented 2 years ago

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.

lovettchris commented 2 years ago

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

image

and most other parts of vscode have their own explicit 'font size' properties.... (markdown preview, debug console, terminal, etc).

gebner commented 2 years ago

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!

leodemoura commented 2 years ago

Marked as a low priority since none of the actual users asked for this feature.

linesthatinterlace commented 5 months ago

Just a note to say I'm an actual user and I would love this feature!