-
Notifications
You must be signed in to change notification settings - Fork 15
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Feature Request: use different font #7
Comments
All I had to do was change the browser font myself... Sorry, I didn't realise that. |
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? |
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) |
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. |
Currently Mac-users also have a hard time because for most of them it does not load a mono-space font. |
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? |
I realised that 'Droid Sans Mono' was just a random font on my computer. I did change the editor to use Could you test at https://lean.math.hhu.de/ and see if it all looks good @Seasawher ? |
Thanks for the quick response. I have tested it. I found a problem: When you try to define 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 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. |
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. |
I think this issue itself has been resolved. |
I am always grateful to lean4web. Thanks.
It would look even more beautiful if fonts like JuliaMono could be used.
https://juliamono.netlify.app/
The text was updated successfully, but these errors were encountered: