While implementing #3925, I noticed that the performance of the
`textDocument/semanticTokens/full` request is *extremely* bad due to a
quadratic implementation. Specifically, on my machine, computing the
full semantic tokens for `Lean/Elab/Do.lean` took a full 5s. In
practice, this means that while elaborating the file, one core is
entirely busy with computing the semantic tokens for the file.
This PR fixes this performance bug by re-implementing the semantic token
handling, reducing the latency for `Lean/Elab/Do.lean` from 5s to 60ms.
As a result, the overly cautious refresh latency of 5s in #3925 can
easily be reduced to 2s again.
Since the previous semantic tokens implementation used a very brittle
hack to identify projections, this PR also changes the projection
notation elaboration to augment the `InfoTree` syntax for the field of a
projection with a special syntax node of kind
`Lean.Parser.Term.identProjKind`. With this syntax kind, projection
fields can now easily be identified in the `InfoTree`.
faa4d16dc1