VSCode extension: highlighting in import line

Stream: general

[Michael Stoll]

In the line

import Mathlib.GroupTheory.Perm.Cycle.Type

the Type part is highlighted in blue (in VSCode with Lean4 extebsion v0.0.160), which looks a bit strange as here it is part of a module name and not a keyword.

[Yaël Dillies]

It is also highlighted differently here on Zulip!

[Michael Stoll]

But the highlighting is VSCode is supposed to be smart...

[Yaël Dillies]

Just to clarify, all I am saying is that the bug is also present in the pygments version that Zulip uses

[Eric Wieser]

Vscode highlights are dumb + smart

[Eric Wieser]

If the smart layer doesn't have anything to say, the dumb layer wins

[Patrick Massot]

Here it is clearly the regex based dumb stuff speaking.

[Eric Wieser]

Yes, in this case we should teach the dumb highlighter to be smarter (because it's standard syntax and affects Zulip), but in some cases of custom syntax the only reasonable thing to do is to teach the smart stuff to be more talkative

[Eric Wieser]

I don't know if the semantic highlighting can say "this is regular text"

[Julian Berman]

In lean.nvim the dumb highlighting we have gets this right, mostly because we tell it . is an identifier character. Perhaps "just" doing something similar in VSCode is the fix (e.g. adding a lookbehind perhaps to Type?)