Zulip Chat Archive

Stream: new members

Topic: Unicode on Mac


view this post on Zulip Duckki Oe (Dec 03 2020 at 20:20):

I wonder how you set up VS Code on Mac to see unicode unbroken.
Several unicode symbols look broken on my Mac. For example, the multiset cons notation appears as a box.

infixr ` :: `:67  := multiset.cons

image.png

It also appears broken on Mathlib HTML document on Safari, too.
image.png

view this post on Zulip Duckki Oe (Dec 03 2020 at 20:21):

I use "SF Mono" font on VS Code and Safari is using the system default font. But, changing font setting doesn't seem to help.

view this post on Zulip Bryan Gin-ge Chen (Dec 03 2020 at 20:22):

I'm using Source Code Variable and DejaVu Sans Mono from the list here and things seem to be OK: https://github.com/leanprover/vscode-lean#other-potentially-helpful-settings

view this post on Zulip Duckki Oe (Dec 03 2020 at 20:22):

Unicode inspector tells me the box is supposed be a subscript "m".
BTW, subscript "v" (\_v in VS code) works for me.

view this post on Zulip Duckki Oe (Dec 03 2020 at 20:23):

Thank, Bryan. I'll try that.

view this post on Zulip Bryan Gin-ge Chen (Dec 03 2020 at 20:24):

In Firefox and Chrome I also chose Deja Vu Sans Mono as the default monospace font; you might have to make a similar change in Safari.

view this post on Zulip Duckki Oe (Dec 03 2020 at 20:36):

Simply installing Deja Vu Sans Mono fixed the problem on VS code and Chrome. Thanks, @Bryan Gin-ge Chen
Safari is still refusing to use it, though :(


Last updated: May 11 2021 at 22:14 UTC