web editor font family and size

Stream: lean4

[Shreyas Srinivas]

Two questions:

1. What is the current default font family and font size in the web editor. See screenshot (
   web-editor-sample-for-font.pdf)

2. Is it possible to change the font size? Is such a feature in the pipeline?

[Richard Copley]

The web app doesn't serve its own fonts, so it is up to your browser to choose one of your installed fonts to implement the CSS style. That text's CSS style has has font-family Consolas, "Courier New", monospace and font-size 14px. (Depending on your browser, you might be able to shift-(right click) on the text to bring up the context menu and click "Inspect" to check this.)

For me, here, the text is displayed in Consolas, but that is not what is in your screenshot. That looks like Bitstream Vera Sans Mono.

[Jon Eugster]

Currently, there's no new feature planned, but you're very welcome to contribute one! (here: lean4web)

you can also dm me if you have questions about the code :)

[Shreyas Srinivas]

Jon Eugster said:

Currently, there's no new feature planned, but you're very welcome to contribute one! (here: lean4web)

you can also dm me if you have questions about the code :)

I'd love to. Currently I am swamped with work. If this issue remains unresolved till mid March, I will probably give it a try.

[Eric Rodriguez]

image.png

Is there any way to change the infoview font?

[Kevin Buzzard]

There must be, because that's not the font I have :-)

[František Silváši 🦉]

You can style it with CSS with Lean4 > Infoview: Styleoption.
E.g. body { font-family: "Comic Sans MS", "Comic Sans"; }