Semantic Highlighting of Literals

Stream: lean4

[Julian Berman]

I should probably do a bit more digging before asking, but sorry, being lazy this afternoon --

Is there anything special about how the Lean 4 LSP sends semantic highlighting of string and number literals? I'm trying to diagnose why I don't see any highlighting of them (whereas everything else I see works AFAICT).

(n.b. this is in neovim, so a possible diagnosis is "the tokens are getting lost after the LSP sends them", but yeah it's only happening for string literals and numbers)

[Sebastian Ullrich]

They don't have semantic highlighting. Does that count as special?

[Julian Berman]

Aha! It does, I suspected as much. So in VSCode, they're highlighted separately/statically?