Zulip Chat Archive
Stream: new members
Topic: Unicode on Mac
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
It also appears broken on Mathlib HTML document on Safari, too.
image.png
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.
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
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.
Duckki Oe (Dec 03 2020 at 20:23):
Thank, Bryan. I'll try that.
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.
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: Dec 20 2023 at 11:08 UTC