## Stream: Zulip meta

### Topic: syntax highlighting

#### Adam Topaz (Dec 06 2023 at 13:23):

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 (Dec 06 2023 at 13:27):

Another question: does anyone actually like the new colours?

#### Eric Wieser (Dec 06 2023 at 13:28):

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 (Dec 06 2023 at 13:33):

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 (Dec 06 2023 at 13:33):

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

#### Alex J. Best (Dec 06 2023 at 13:36):

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 (Dec 06 2023 at 13:37):

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

#### Adam Topaz (Dec 06 2023 at 13:38):

The mobile version still uses the old colours

#### Alex J. Best (Dec 06 2023 at 13:44):

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

#### Eric Wieser (Dec 06 2023 at 13:46):

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

#### Alya Abbott (Dec 06 2023 at 16:45):

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

#### Eric Wieser (Dec 06 2023 at 17:29):

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 (Dec 06 2023 at 17:30):

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 (Dec 06 2023 at 17:59):

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

Last updated: Dec 20 2023 at 11:08 UTC