diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 0cd61b7c78..904e21eb7f 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -324,14 +324,20 @@ where
           stx.getArgs.forM go
   highlightId (stx : Syntax) : ReaderT SemanticTokensContext (StateT SemanticTokensState RequestM) _ := do
     if let some range := stx.getRange? then
+      let mut lastPos := range.start
       for ti in (← read).snap.infoTree.deepestNodes (fun
         | _, i@(Elab.Info.ofTermInfo ti), _ => match i.pos? with
           | some ipos => if range.contains ipos then some ti else none
           | _         => none
         | _, _, _ => none) do
-        match ti.expr with
-        | Expr.fvar .. => addToken ti.stx SemanticTokenType.variable
-        | _            => if ti.stx.getPos?.get! > range.start then addToken ti.stx SemanticTokenType.property
+        if let Expr.fvar .. := ti.expr then
+          addToken ti.stx SemanticTokenType.variable
+        else if ti.stx.getPos?.get! > lastPos then
+          -- any info after the start position: must be projection notation
+          addToken ti.stx SemanticTokenType.property
+          -- avoid reporting same position twice; the info node can occur multiple times if
+          -- e.g. the term is elaborated multiple times
+          lastPos := ti.stx.getPos?.get!
   highlightKeyword stx := do
     if let Syntax.atom info val := stx then
       if val.bsize > 0 && val[0].isAlpha then