Tooling: What does semantic highlighting?

Stream: lean4

[Max Nowak]

I was wondering how difficult it would be to add some better semantic highlighting, so I embarked on a journey through the VSCode Lean extension and the Lean Server code. While I can find all kinds of cool stuff like hover support, etc, I just can't figure out where the semantic highlighting happens.

[Gabriel Ebner]

It's this function on the server side: https://github.com/leanprover/lean4/blob/fad21a4cda3c6926e37ec01e518d541c7681a652/src/Lean/Server/FileWorker/RequestHandling.lean#L335

[Max Nowak]

Nice! I will definitely have a closer look at it, though it is a lot at once :sweat_smile:. Where in the VSCode extension are the semantic tokens received?