Zulip Chat Archive

Stream: general

Topic: arrow font


view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:23):

arrows.png

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?

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:23):

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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:25):

Hmm, those are indeed quite similar.

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:26):

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

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:26):

Not sure if it will help

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:26):

I'm fond of "Solarized"

view this post on Zulip Jesse Michael Han (Dec 14 2019 at 19:27):

they look very different in my emacs:

pasted image

view this post on Zulip Jesse Michael Han (Dec 14 2019 at 19:27):

i'm using Source Code Pro

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:58):

Maybe it's time I switched back

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 14 2019 at 20:12):

I'm not at my Lean box currently

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 21:12 UTC