VSCode: Where is semantic highlighting?

Stream: lean4

[Chris Lovett]

The 'textDocument/semanticTokens/full' request comes directly from VSCode and goes to the LSP and back to VSCode without the extension being involved at all. You might be able to intercept them in the LeanClient if you insert the (SemanticTokensMiddleware).