Zulip Chat Archive

Stream: general

Topic: arrow font

Kevin Buzzard (Dec 14 2019 at 19:23):

Am I just stupid that I can't tell the difference between those two arrows? Can someone just tell me how to make one of them bright orange or something?

Kevin Buzzard (Dec 14 2019 at 19:23):

I'm on Ubuntu and I think I need new glasses.

Kevin Buzzard (Dec 14 2019 at 19:24):

import topology.category.Top.opens

universes v u

open category_theory

variables (C : Type u) [𝒞 : category.{v} C] (A : C)
include 𝒞

example : C → C := id
example : A ⟶ A := 𝟙 A

Kevin Buzzard (Dec 14 2019 at 19:25):

Ha I'd even be happy if the category one just had a big red box around it in VS Code like the above :rolling_on_the_floor_laughing:

Johan Commelin (Dec 14 2019 at 19:25):

Hmm, those are indeed quite similar.

Johan Commelin (Dec 14 2019 at 19:26):

You can play with Ctrl-Shift-P "Colorscheme"

Johan Commelin (Dec 14 2019 at 19:26):

Not sure if it will help

Johan Commelin (Dec 14 2019 at 19:26):

I'm fond of "Solarized"

Jesse Michael Han (Dec 14 2019 at 19:27):

they look very different in my emacs:

pasted image

Jesse Michael Han (Dec 14 2019 at 19:27):

i'm using Source Code Pro

Jesse Michael Han (Dec 14 2019 at 19:35):

you can change the color by assigning that character to another face, like so:

pasted image

Jesse Michael Han (Dec 14 2019 at 19:44):

oh, i forgot Kevin is the lifelong emacs user who uses VSCode for Lean :P

you might still have better luck with Source Code Pro as your font

Kevin Buzzard (Dec 14 2019 at 19:57):

The reason I switched from emacs to VS Code despite literally decades of experience with emacs was that I wanted to know the system which my students were using very well so I could help them

Kevin Buzzard (Dec 14 2019 at 19:58):

Maybe it's time I switched back

Bryan Gin-ge Chen (Dec 14 2019 at 20:01):

I saw the same thing as Kevin (except in a dark theme) with "Deja Vu Sans Mono" as the first font in my list, but I see this, when I use "Source Code Variable" instead:

Screenshot-2019-12-14-14.45.58.png

@Johan Commelin you said that the two arrows are different colors in your VS Code? It's strange that Kevin and I both see them as the same color. I noticed that the arrows are highlighted as constants in the emacs mode, but not in the VS Code extension's syntax highlighting. The only appearance of → in that file is where it's used to help find function / theorem names on line 83.

Johan Commelin (Dec 14 2019 at 20:12):

@Bryan Gin-ge Chen I didn't actually check... In my memory they were different colours. But maybe that's only here on Zulip.

Johan Commelin (Dec 14 2019 at 20:12):

I'm not at my Lean box currently

Bryan Gin-ge Chen (Dec 14 2019 at 20:14):

We could certainly make the usual \to arrow a different color if it'd be helpful.

Mario Carneiro (Dec 14 2019 at 20:21):

They are recognizable in zulip because the long arrow has an error box around it :P

Last updated: Dec 20 2023 at 11:08 UTC