syntax highlighting

Stream: Zulip meta

[Adam Topaz]

Did the syntax highlighting colours on zulip change for anyone else recently? Here's what it looks like on my computer, starting today:
Screenshot-2023-12-06-at-06-22-33-750-Is-there-code-for-X-Lean-Zulip.png

[Adam Topaz]

Another question: does anyone actually like the new colours?

[Eric Wieser]

From:

Heather Macbeth said:

I can give you a proof with an "explicit" witness:

import Mathlib.Tactic.Polyrith
import Mathlib.RingTheory.Int.Basic

open Int hiding gcd gcd_dvd_left gcd_dvd_right

lemma foo {a b c : ℤ} (hb : b ≠ 0) (h : a * b^2 = c^2) : IsSquare a  := by
  obtain ⟨k, hk⟩ : ∃ k, b = gcd b c * k := gcd_dvd_left b c
  obtain ⟨l, hl⟩ : ∃ l, c = gcd b c * l  := gcd_dvd_right b c
  use a * k * gcdB b c + l * gcdA b c
  have hd : gcd b c ≠ 0 := fun hd => hb (by simpa [hd] using hk)
  apply mul_right_cancel₀ (pow_ne_zero 2 hd)
  have H : gcd b c = b * gcdA b c + c * gcdB b c := Int.gcd_eq_gcd_ab b c
  polyrith

[Eric Wieser]

https://github.com/zulip/zulip/pull/26898 looks like it changed the color scheme, though I don't see much discussion there about why

[Adam Topaz]

It's not a huge deal to be fair, but I find the new colours harder to read.

[Alex J. Best]

Yeah I'm also not sure if that's just lack of familiarity, it would be nice to get a side by side comparison

[Adam Topaz]

33D22C0C-7CE3-40E5-A6DF-EACA32A0364A.png

[Adam Topaz]

The mobile version still uses the old colours

[Alex J. Best]

Yeah personally I definitely prefer that, the new highlights seem way too bright and bold for keywords

[Eric Wieser]

Odd that the opeartors lost highlights in some place but not others

[Alya Abbott]

There's extensive discussion in the Zulip development community thread linked from the PR, if anyone is curious about the background.

[Eric Wieser]

Here's the relevant message:
@Greg Price said:

The "default" style looks good to me. Among the dark styles, all of "monokai" and "lightbulb" and "github-dark" look fine, and personally I'd probably choose "lightbulb".

[Eric Wieser]

I think probably a lot of people here would have preferred github dark because the code we look at is often on github anyway, but I understand that may not apply to all zulip instances!

[Alex J. Best]

It sounds like a more reasonable feature request might therefore be to offer these different highlight themes as options to the user (with a sensible default) then