Semantic syntax highlighting / color scheme, also in Output

Stream: general

[Moritz R]

Is there anything i can do to get this https://github.com/leanprover/lean4/issues/2305 work from Kiiyya any further to integration?
I think more fine grained coloring could really help with parsing formulas - especially in the output, where we have no colors at all atm.

[Max Nowak 🐉]

I’ve been using my own fork of Lean for years now just to get my gay colors :D. And I’m slowly tweaking the colors as well, for example having a slightly different hue for inductive types vs structure-like types.

[Max Nowak 🐉]

I hadn’t posted the code for the better highlighting, because it’s not very high quality code and it might have performance issues on edge cases. I’m slowly working on a small refactor.

[Max Nowak 🐉]

But I’d love for Lean to have this out of the box.

[Max Nowak 🐉]

I would be curious whether we could have semantic highlighting in the infoview as well.

[Moritz R]

i can't see any reason why this shouldn't be able to pass the neccessary information to the infoview

[Moritz R]

image.png
This is what the infoview ("output") in isabelle might look like, and i think these few colors already make it much more legible

[Moritz R]

compared to

proof (prove)
goal (6 subgoals):

1. ⋀a. ⟦i1 = Some a; i2 = None⟧ ⟹ i1 ∈ γ_bounds (B A1')
2. ⋀a aa. ⟦i1 = Some a; i2 = Some aa⟧ ⟹ i1 ∈ γ_bounds (B A1')
3. ⟦i1 = None; i2 = None⟧ ⟹ i2 ∈ γ_bounds (B A2')
4. ⋀a. ⟦i1 = None; i2 = Some a⟧ ⟹ i2 ∈ γ_bounds (B A2')
5. ⋀a. ⟦i1 = Some a; i2 = None⟧ ⟹ i2 ∈ γ_bounds (B A2')
6. ⋀a aa. ⟦i1 = Some a; i2 = Some aa⟧ ⟹ i2 ∈ γ_bounds (B A2')

[Max Nowak 🐉]

It really does make it more legible, I agree. (I also wish we had a LaTeX-like view with big operators, subscripts, better spacing etc., but that's perhaps another discussion yet.)