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

fix: highlight keywords when keyword is actual identifier (#9019)

Browse source 
This PR fixes a bug where semantic highlighting would only highlight
keywords that started with an alphanumeric character. Now, it uses
`Lean.isIdFirst`.
This commit is contained in:
Marc Huisinga 2025-06-27 10:23:10 +02:00 • committed by GitHub
parent 1a6eae16ec
commit 1edb7632b5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Server/FileWorker/SemanticHighlighting.lean
View file

@ -110,8 +110,8 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema
stx.getArgs.map collectSyntaxBasedSemanticTokens |>.flatten
let Syntax.atom _ val := stx
| return tokens
let isRegularKeyword := val.length > 0 && val.front.isAlpha
let isHashKeyword := val.length > 1 && val.front == '#' && (val.get ⟨1⟩).isAlpha
let isRegularKeyword := val.length > 0 && isIdFirst val.front
let isHashKeyword := val.length > 1 && val.front == '#' && isIdFirst (val.get ⟨1⟩)
if ! isRegularKeyword && ! isHashKeyword then
return tokens
return tokens.push ⟨stx, keywordSemanticTokenMap.findD val .keyword⟩