Feature Request: use different font

[Seasawher]

I am always grateful to lean4web. Thanks.

It would look even more beautiful if fonts like JuliaMono could be used. https://juliamono.netlify.app/

[Seasawher]

All I had to do was change the browser font myself... Sorry, I didn't realise that.

[Seasawher]

Not everyone can conceive of installing a font and changing the settings in their browser. Wouldn't it be nice to choose a font that displays Unicode readably by default?

[joneugster]

It would be very reasonable to have a reasonable default font!

(not google though, I believe there is something about google fonts not bein GDPR conform or some nonesense like that)

[Seasawher]

My mother tongue is Japanese and I usually use the font Juisee for Lean.

See https://github.com/yuru7/juisee

It would be preferable if this could be made convenient for non-English speakers.

[joneugster]

I'd happily accept a PR that adds the correct fonts. working on it right now :)

Currently Mac-users also have a hard time because for most of them it does not load a mono-space font.

[joneugster]

On my end it looks very reasonable, doesn't it?

CSS says: font-family: "Droid Sans Mono", "monospace", monospace

Do you think it would be satisfactory to just ship "droid sans mono" together with the bundle?

[Seasawher]

Sorry, I don't know how to install Droid Sans Mono and can't try it myself.

Looks good, but do the Unicode symbols used in mathematics show up clearly?

[joneugster]

I realised that 'Droid Sans Mono' was just a random font on my computer. I did change the editor to use JuliaMono now.

Could you test at https://lean.math.hhu.de/ and see if it all looks good @Seasawher ?

[Seasawher]

Thanks for the quick response. I have tested it.

I found a problem:

When you try to define longlonglong....name, there was a problem with the cursor "lagging" behind the displayed character.

In the image above, the cursor is shown as being in the middle of the line, but it actually exists at the end of the line.

see https://lean.math.hhu.de/#code=def%20longlonglonglonglonglonglonglonglongname%20%3A%3D%22hoge%22%0D%0A%0D%0A

[Seasawher]

I found another problem... I think this is a bug in Julia Mono rather than in Lean4 Web, but the kanji character for "点" (which means "dot") is displayed incorrectly.

see: https://github.com/cormullion/juliamono/issues/206

[joneugster]

In the image above, the cursor is shown as being in the middle of the line, but it actually exists at the end of the line.

I cannot reproduce this on my end. Could it be some local (CSS) caching? If it persists, please open a new issue about it!

Regarding "点" , reading the linked issue, I think we just need to update the font in a few weeks.

[Seasawher]

I think this issue itself has been resolved.