max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: semantic highlighting of projection notation elaborated twice

Browse source
This commit is contained in:
Sebastian Ullrich 2021-11-23 13:01:51 +01:00
parent 9ae6380b43
commit 226121433f
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Server/FileWorker/RequestHandling.lean
View file

@ -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