From 1edb7632b5ff76028669b26151b71ca919ee92db Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 27 Jun 2025 10:23:10 +0200 Subject: [PATCH] fix: highlight keywords when keyword is actual identifier (#9019) This PR fixes a bug where semantic highlighting would only highlight keywords that started with an alphanumeric character. Now, it uses `Lean.isIdFirst`. --- src/Lean/Server/FileWorker/SemanticHighlighting.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index 8453e05898..9fca1502a3 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -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⟩