Open wadler opened 6 years ago
Source Code (v2.030) does not support any of those arrow characters, so what you're getting is from a different font.
Aha! Thank you. Any chance that it could support them? Apologies for a newbie question, but how do I check which characters are in the font and which are not?
There are a few sites to test font files, among them https://wakamaifondue.com/ https://fontdrop.info
That said, it is difficult to support double-or triple-width characters in a true monospaced font. If not all glyphs have the same width, some environments won’t recognize the font as a monospaced font anymore.
Thank you to miguelsousa and frankrolf for the additional explanations.
That said, it is difficult to support double-or triple-width characters in a true monospaced font. If not all glyphs have the same width, some environments won’t recognize the font as a monospaced font anymore.
Certain characters (Emoji, CJK Kanji, some grapheme clusters, and others) are expected to be double-width in an otherwise monospace context. Ideally one would like to have monospace full-width (double-width) fonts that are designed to be used along with a matching monospace font.
Currently, long arrows (⟵ ⟸ ⟶ ⟹) have a length about 11/12 of the monospaced characters. For laying out code (e.g., in Agda) it would be extremely helpful if their length was an exact multiple of a monospace, with 3 characters wide being the obvious choice.
Similarly, floor and ceiling brackets (⌊ ⌋ ⌈ ⌉) have a width about 5/6 of the monospaced characters. Again, it would be extremely helpful if they were the same width as all the monospaced characters.
I am writing an online textbook for which Source Code Pro would be the perfect choice, if these issues were fixed. Thank you for creating Source Code Pro, which looks beautiful!