Zulip Chat Archive

Stream: lean4

Topic: Tooling: What does semantic highlighting?


Max Nowak (May 26 2022 at 11:44):

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 (May 26 2022 at 11:46):

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

Max Nowak (May 26 2022 at 12:31):

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?


Last updated: Dec 20 2023 at 11:08 UTC