From 392ff2405fb1f5a6328b9610e854f641064413ea Mon Sep 17 00:00:00 2001 From: ivance Date: Sun, 1 Nov 2026 20:16:12 +0800 Subject: [PATCH 1/2] feat: improve semantic highlighting --- .../FileWorker/SemanticHighlighting.lean | 150 +++++++++-- tests/server_interactive/semanticTokens.lean | 6 +- .../semanticTokens.lean.out.expected | 101 ++++++-- ...manticTokensMarkdownDocs.lean.out.expected | 30 +++ ...nticTokensMarkdownIndent.lean.out.expected | 10 + .../semanticTokensVersoDocs.lean.out.expected | 236 +++++++++++++++--- ...anticTokensVersoDocument.lean.out.expected | 109 +++++++- 7 files changed, 575 insertions(+), 67 deletions(-) diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index bb6d087c6f4f..76de109a0803 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -817,10 +817,11 @@ without elaboration information. partial def collectSyntaxBasedSemanticTokens (text : FileMap) : (stx : Syntax) → Array LeanSemanticToken | `($e.$id:ident) => let tokens := collectSyntaxBasedSemanticTokens text e - emitSyntaxToken tokens id .property + -- Prefer the elaborated declaration kind over this syntactic fallback. + emitSyntaxToken tokens id .property (priority := 4) | `($e |>.$field:ident) => let tokens := collectSyntaxBasedSemanticTokens text e - emitSyntaxToken tokens field .property + emitSyntaxToken tokens field .property (priority := 4) | stx => Id.run do if noHighlightKinds.contains stx.getKind then return #[] @@ -862,25 +863,140 @@ partial def collectSyntaxBasedSemanticTokens (text : FileMap) : (stx : Syntax) return tokens return emitSyntaxToken tokens stx (keywordSemanticTokenMap.getD val .keyword) +private partial def forallBody : Expr → Expr + | .forallE _ _ body _ => forallBody body + | type => type + +private def typeForSortResult? (type : Expr) : Option SemanticTokenType := + match forallBody type with + | .sort u => + if u.isAlwaysZero then + some .enum + else + some .type + | _ => none + +private partial def typeExprResult? (env : Environment) (lctx : LocalContext) (type : Expr) : + Option SemanticTokenType := + match typeForSortResult? type with + | some tokenType => some tokenType + | none => + match type.getAppFn with + | .const declName us => + match env.find? declName with + | some info => typeForSortResult? (info.instantiateTypeLevelParams us) + | none => none + | .fvar fvarId => + match lctx.find? fvarId with + | some localDecl => typeForSortResult? localDecl.type + | none => none + | _ => none + +private def classifyLocal (env : Environment) (ti : Elab.TermInfo) (localDecl : LocalDecl) : + Option SemanticTokenType := Id.run do + let localType := localDecl.type + -- Recall that `isAuxDecl` is used for declarations currently being elaborated, e.g. recursive + -- functions and inductive types while their constructors are being processed. + if localDecl.isAuxDecl then + if let some tokenType := typeForSortResult? localType then + return some tokenType + else + return some .function + if let some tokenType := typeForSortResult? localType then + if localType.isSort && tokenType == .type then + return some .typeParameter + else + return some tokenType + if localDecl.isImplementationDetail then + return none + if typeExprResult? env ti.lctx localType == some .enum then + return some .variable + if ti.isBinder then + return some .parameter + return some .variable + +private def classifyConstant (env : Environment) (declName : Name) (info : ConstantInfo) (expr : Expr) : + SemanticTokenType := + if env.isProjectionFn declName then + .property + else match info with + | .ctorInfo _ => .enumMember + | .inductInfo info => + if isClass env info.name then + .interface + else if isStructure env info.name then + .struct + else if let some tokenType := typeExprResult? env {} expr then + tokenType + else + .type + | .thmInfo _ | .recInfo _ => .function + | _ => + if let some tokenType := typeExprResult? env {} expr then + tokenType + else + .function + +private def findConstInfoWithEnv? (ctx : Elab.ContextInfo) (declName : Name) : + Option (Environment × ConstantInfo) := + match ctx.env.find? declName with + | some info => some (ctx.env, info) + | none => ctx.cmdEnv?.bind fun env => (env.find? declName).map (env, ·) + +private def getSemanticTokenSyntax (stx : Syntax) : Syntax := + if stx.isOfKind Parser.Term.identProjKind then + stx[0] + else match stx with + | `(Parser.Command.declId|$id$[.{$_ls,*}]?) => id.raw + | `(.$id:ident) | `(.$id:ident.{$_us,*}) => id.raw + | _ => stx + +private def getAppFnSyntax? (stx : Syntax) : Option Syntax := + if stx.isOfKind ``Parser.Term.app then + some stx[0] + else + none + +private def collectTermInfoBasedSemanticToken (ctx : Elab.ContextInfo) (ti : Elab.TermInfo) : + Option LeanSemanticToken := Id.run do + let stx := getSemanticTokenSyntax ti.stx + if ti.expr.isSort then + let .original .. := stx.getHeadInfo + | return none + return LeanSemanticToken.ofSyntax? stx .class + match ti.expr.getAppFn with + | Expr.fvar fvarId .. => + let some localDecl := ti.lctx.find? fvarId + | return none + let some stx := + if let `($_:ident) := stx then + some stx + else if localDecl.isAuxDecl then + getAppFnSyntax? stx + else + none + | return none + let .original .. := stx.getHeadInfo + | return none + let `($_:ident) := stx + | return none + return (classifyLocal ctx.env ti localDecl).bind (LeanSemanticToken.ofSyntax? stx ·) + | Expr.const declName .. => + let `($_:ident) := stx + | return none + let .original .. := stx.getHeadInfo + | return none + match findConstInfoWithEnv? ctx declName with + | some (env, info) => return LeanSemanticToken.ofSyntax? stx (classifyConstant env declName info ti.expr) + | none => return none + | _ => return none + /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken := - List.toArray <| i.deepestNodes fun _ info _ => do + List.toArray <| i.deepestNodes fun ctx info _ => do let .ofTermInfo ti := info | none - let .original .. := ti.stx.getHeadInfo - | none - if let `($_:ident) := ti.stx then - if let Expr.fvar fvarId .. := ti.expr then - if let some localDecl := ti.lctx.find? fvarId then - -- Recall that `isAuxDecl` is an auxiliary declaration used to elaborate a recursive definition. - if localDecl.isAuxDecl then - if ti.isBinder then - return (← LeanSemanticToken.ofSyntax? ti.stx .function) - else if ! localDecl.isImplementationDetail then - return (← LeanSemanticToken.ofSyntax? ti.stx .variable) - if ti.stx.getKind == Parser.Term.identProjKind then - return (← LeanSemanticToken.ofSyntax? ti.stx .property) - none + collectTermInfoBasedSemanticToken ctx ti /-- A debugging utility for inspecting sets of collected tokens, classified by line and sorted by diff --git a/tests/server_interactive/semanticTokens.lean b/tests/server_interactive/semanticTokens.lean index b50d09157bf6..4343eeae8663 100644 --- a/tests/server_interactive/semanticTokens.lean +++ b/tests/server_interactive/semanticTokens.lean @@ -1,8 +1,10 @@ +/-! This file tests semantic token kinds. -/ + def foo1 (x : Nat) := x.succ -def foo2 (x : Nat) := x |>.succ +def foo2 (x : Nat) : List Nat := .cons.{0} (x |>.succ) .nil theorem foo3 (x : Nat) : True := let y := x.succ - True.intro + .intro #eval 1 --^ collectDiagnostics diff --git a/tests/server_interactive/semanticTokens.lean.out.expected b/tests/server_interactive/semanticTokens.lean.out.expected index eac7701442d0..e49c645d34c5 100644 --- a/tests/server_interactive/semanticTokens.lean.out.expected +++ b/tests/server_interactive/semanticTokens.lean.out.expected @@ -5,50 +5,65 @@ [{"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 2, "character": 0}, "end": {"line": 3, "character": 0}}, + {"start": {"line": 4, "character": 0}, "end": {"line": 5, "character": 0}}, "message": "Goals accomplished!", "leanTags": [2], "isSilent": true, "fullRange": - {"start": {"line": 2, "character": 0}, "end": {"line": 4, "character": 12}}}, + {"start": {"line": 4, "character": 0}, "end": {"line": 6, "character": 8}}}, {"tags": [1], "source": "Lean 4", "severity": 2, "range": - {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}, + {"start": {"line": 5, "character": 6}, "end": {"line": 5, "character": 7}}, "message": "Variable name `y` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _y\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`", "fullRange": - {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}}, + {"start": {"line": 5, "character": 6}, "end": {"line": 5, "character": 7}}}, {"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 5}}, + {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 5}}, "message": "1", "fullRange": - {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 5}}}]} + {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 5}}}]} {"textDocument": {"uri": "file:///semanticTokens.lean"}, - "position": {"line": 6, "character": 2}} + "position": {"line": 8, "character": 2}} {"data": [0, + 4, + 37, + 24, + 0, + 2, 0, 3, 0, 0, 0, - 10, - 1, + 4, + 4, + 3, + 0, + 0, + 6, 1, + 11, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, 0, 2, 4, - 2, + 12, 0, 1, 0, @@ -56,19 +71,49 @@ 0, 0, 0, - 10, - 1, + 4, + 4, + 3, + 0, + 0, + 6, 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 7, + 4, + 5, + 0, + 0, + 5, + 3, + 5, 0, 0, + 8, + 4, 12, + 0, + 0, + 10, 1, 1, 0, 0, 5, 4, - 2, + 12, + 0, + 0, + 7, + 3, + 12, 0, 1, 0, @@ -76,9 +121,24 @@ 0, 0, 0, - 14, - 1, + 8, + 4, + 3, + 0, + 0, + 6, 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 7, + 4, + 7, 0, 1, 2, @@ -88,7 +148,7 @@ 0, 4, 1, - 1, + 11, 0, 0, 5, @@ -98,9 +158,14 @@ 0, 2, 4, - 2, + 12, 0, + 1, 3, + 5, + 12, + 0, + 2, 0, 5, 0, diff --git a/tests/server_interactive/semanticTokensMarkdownDocs.lean.out.expected b/tests/server_interactive/semanticTokensMarkdownDocs.lean.out.expected index c3106a6a53e3..df8a8b0c789e 100644 --- a/tests/server_interactive/semanticTokensMarkdownDocs.lean.out.expected +++ b/tests/server_interactive/semanticTokensMarkdownDocs.lean.out.expected @@ -1025,11 +1025,26 @@ 3, 0, 0, + 0, + 4, + 1, + 3, + 0, 2, 0, 3, 0, 0, + 0, + 4, + 1, + 3, + 0, + 0, + 5, + 1, + 3, + 0, 1, 0, 5, @@ -1120,6 +1135,11 @@ 3, 0, 0, + 0, + 4, + 12, + 3, + 0, 2, 4, 20, @@ -1160,6 +1180,11 @@ 3, 0, 0, + 0, + 4, + 10, + 3, + 0, 3, 0, 56, @@ -1210,6 +1235,11 @@ 3, 0, 0, + 0, + 4, + 9, + 3, + 0, 3, 0, 1, diff --git a/tests/server_interactive/semanticTokensMarkdownIndent.lean.out.expected b/tests/server_interactive/semanticTokensMarkdownIndent.lean.out.expected index fa999e756c38..f60bfbc82e0b 100644 --- a/tests/server_interactive/semanticTokensMarkdownIndent.lean.out.expected +++ b/tests/server_interactive/semanticTokensMarkdownIndent.lean.out.expected @@ -41,6 +41,11 @@ 3, 0, 0, + 0, + 4, + 14, + 3, + 0, 3, 0, 53, @@ -60,4 +65,9 @@ 0, 3, 0, + 0, + 0, + 4, + 14, + 3, 0]} diff --git a/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected b/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected index 32b78c08c263..39faa1db8efc 100644 --- a/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected +++ b/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected @@ -161,19 +161,64 @@ 0, 0, 0, - 14, + 4, + 8, + 3, + 0, + 0, + 10, 7, 1, 0, + 0, + 10, + 12, + 5, + 0, + 0, + 15, + 12, + 3, + 0, + 0, + 16, + 4, + 5, + 0, + 0, + 6, + 5, + 5, + 0, + 0, + 6, + 10, + 5, + 0, + 0, + 11, + 9, + 5, + 0, 1, - 14, + 3, + 6, + 12, + 0, + 0, + 11, 7, 1, 0, 0, 8, 4, - 2, + 3, + 0, + 0, + 5, + 9, + 3, 0, 2, 4, @@ -198,7 +243,7 @@ 0, 1, 4, - 29, + 3, 0, 0, 4, @@ -232,11 +277,16 @@ 4096, 0, 1, - 5, + 4, + 3, + 0, + 0, + 4, + 1, 29, 0, 0, - 5, + 1, 1, 1, 0, @@ -272,11 +322,16 @@ 4096, 0, 1, - 10, + 4, + 3, + 0, + 0, + 4, + 6, 29, 0, 0, - 10, + 6, 1, 0, 4096, @@ -291,19 +346,29 @@ 0, 0, 0, - 10, + 4, + 4, + 3, + 0, + 0, + 6, 1, 1, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, 0, 2, 4, - 2, + 12, 0, 1, 4, @@ -328,7 +393,7 @@ 0, 1, 4, - 29, + 3, 0, 0, 4, @@ -362,11 +427,16 @@ 4096, 0, 1, - 5, + 4, + 3, + 0, + 0, + 4, + 1, 29, 0, 0, - 5, + 1, 1, 1, 0, @@ -402,11 +472,21 @@ 4096, 0, 1, - 11, + 4, + 3, + 0, + 0, + 4, + 3, 29, 0, 0, - 11, + 3, + 4, + 3, + 0, + 0, + 4, 1, 0, 4096, @@ -421,19 +501,29 @@ 0, 0, 0, - 10, + 4, + 4, + 3, + 0, + 0, + 6, 1, 1, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, 0, 5, 4, - 2, + 12, 0, 1, 0, @@ -441,7 +531,17 @@ 0, 0, 0, - 19, + 4, + 4, + 3, + 0, + 0, + 8, + 6, + 3, + 0, + 0, + 7, 5, 0, 0, @@ -677,21 +777,51 @@ 0, 1, 0, - 18, + 10, 30, 0, 0, - 18, + 10, + 3, + 3, + 0, + 0, + 3, + 5, + 30, + 0, + 0, + 5, 1, + 11, + 0, + 0, 1, + 3, + 30, 0, 0, + 3, + 4, + 5, + 0, + 0, + 4, + 2, + 30, + 0, + 0, + 2, 1, - 13, + 3, + 0, + 0, + 1, + 3, 30, 0, 0, - 13, + 3, 1, 1, 0, @@ -1113,7 +1243,7 @@ 0, 1, 1, - 1, + 11, 0, 0, 1, @@ -1193,7 +1323,7 @@ 0, 1, 8, - 29, + 12, 0, 0, 8, @@ -1382,7 +1512,17 @@ 0, 1, 0, - 16, + 4, + 30, + 0, + 0, + 4, + 7, + 3, + 0, + 0, + 7, + 5, 30, 0, 1, @@ -1480,6 +1620,11 @@ 3, 0, 0, + 0, + 4, + 1, + 3, + 0, 3, 0, 97, @@ -1870,6 +2015,16 @@ 3, 0, 0, + 0, + 4, + 11, + 3, + 0, + 0, + 14, + 3, + 5, + 0, 3, 0, 10, @@ -1985,13 +2140,33 @@ 3, 0, 0, + 0, + 4, + 15, + 3, + 0, + 0, + 18, + 3, + 5, + 0, 2, 0, 3, 0, 0, 0, - 38, + 4, + 23, + 3, + 0, + 0, + 27, + 6, + 3, + 0, + 0, + 7, 5, 0, 0, @@ -2089,4 +2264,9 @@ 2, 6, 3, + 0, + 0, + 9, + 3, + 5, 0]} diff --git a/tests/server_interactive/semanticTokensVersoDocument.lean.out.expected b/tests/server_interactive/semanticTokensVersoDocument.lean.out.expected index abf2ca0705f5..40fb5f12f402 100644 --- a/tests/server_interactive/semanticTokensVersoDocument.lean.out.expected +++ b/tests/server_interactive/semanticTokensVersoDocument.lean.out.expected @@ -151,20 +151,95 @@ 0, 0, 0, - 23, - 5, + 4, + 9, + 3, 0, 0, + 12, 6, + 9, 0, + 0, + 7, + 5, + 0, + 0, + 1, + 10, + 23, + 3, + 0, + 1, + 9, + 19, 3, 0, 0, + 20, + 23, 3, 0, + 1, + 4, + 19, 3, 0, 0, + 38, + 4, + 12, + 0, + 0, + 13, + 10, + 3, + 0, + 2, + 27, + 9, + 3, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 23, + 3, + 0, + 0, + 27, + 38, + 3, + 0, + 2, + 23, + 9, + 3, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 19, + 3, + 0, + 0, + 23, + 33, + 3, + 0, + 0, + 34, + 14, + 12, + 0, 2, 4, 49, @@ -195,16 +270,41 @@ 3, 0, 0, + 0, + 4, + 13, + 3, + 0, + 0, + 16, + 6, + 9, + 0, 1, 2, 14, 0, 0, + 0, + 50, + 9, + 3, + 0, 2, 30, 3, 0, 0, + 0, + 4, + 17, + 3, + 0, + 0, + 20, + 29, + 5, + 0, 1, 2, 3, @@ -215,6 +315,11 @@ 1, 0, 0, + 0, + 5, + 4, + 2, + 0, 2, 0, 15, From 9fd0131e3a5fc866afa19afe95bf3bc3b8d428b0 Mon Sep 17 00:00:00 2001 From: ivance Date: Fri, 6 Nov 2026 22:32:52 +0800 Subject: [PATCH 2/2] fix: semantic highlighting inconsistency --- .../FileWorker/SemanticHighlighting.lean | 70 ++- tests/server_interactive/semanticTokens.lean | 27 +- .../semanticTokens.lean.out.expected | 459 +++++++++++++++++- 3 files changed, 507 insertions(+), 49 deletions(-) diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index 76de109a0803..713496d35a6b 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -863,35 +863,26 @@ partial def collectSyntaxBasedSemanticTokens (text : FileMap) : (stx : Syntax) return tokens return emitSyntaxToken tokens stx (keywordSemanticTokenMap.getD val .keyword) -private partial def forallBody : Expr → Expr - | .forallE _ _ body _ => forallBody body - | type => type - private def typeForSortResult? (type : Expr) : Option SemanticTokenType := - match forallBody type with - | .sort u => - if u.isAlwaysZero then - some .enum - else - some .type + (Meta.typeFormerTypeLevelQuick type).map fun u => + if u.isAlwaysZero then .enum else .type + +private partial def typeExprResult? (env : Environment) (lctx : LocalContext) (type : Expr) + (bvarTypes : List Expr := []) : Option SemanticTokenType := + match type.getAppFn with + | .sort _ => typeForSortResult? type + | .forallE _ domain body _ => typeExprResult? env lctx body (domain :: bvarTypes) + | .const declName us => + match env.find? declName with + | some info => typeForSortResult? (info.instantiateTypeLevelParams us) + | none => none + | .fvar fvarId => + match lctx.find? fvarId with + | some localDecl => typeForSortResult? localDecl.type + | none => none + | .bvar idx => bvarTypes[idx]?.bind typeForSortResult? | _ => none -private partial def typeExprResult? (env : Environment) (lctx : LocalContext) (type : Expr) : - Option SemanticTokenType := - match typeForSortResult? type with - | some tokenType => some tokenType - | none => - match type.getAppFn with - | .const declName us => - match env.find? declName with - | some info => typeForSortResult? (info.instantiateTypeLevelParams us) - | none => none - | .fvar fvarId => - match lctx.find? fvarId with - | some localDecl => typeForSortResult? localDecl.type - | none => none - | _ => none - private def classifyLocal (env : Environment) (ti : Elab.TermInfo) (localDecl : LocalDecl) : Option SemanticTokenType := Id.run do let localType := localDecl.type @@ -915,24 +906,24 @@ private def classifyLocal (env : Environment) (ti : Elab.TermInfo) (localDecl : return some .parameter return some .variable -private def classifyConstant (env : Environment) (declName : Name) (info : ConstantInfo) (expr : Expr) : +private def classifyConstant (env : Environment) (info : ConstantInfo) (us : List Level := []) : SemanticTokenType := - if env.isProjectionFn declName then + if env.isProjectionFn info.name then .property else match info with | .ctorInfo _ => .enumMember - | .inductInfo info => + | .inductInfo _ => if isClass env info.name then .interface else if isStructure env info.name then .struct - else if let some tokenType := typeExprResult? env {} expr then + else if let some tokenType := typeForSortResult? (info.instantiateTypeLevelParams us) then tokenType else .type | .thmInfo _ | .recInfo _ => .function | _ => - if let some tokenType := typeExprResult? env {} expr then + if let some tokenType := typeForSortResult? (info.instantiateTypeLevelParams us) then tokenType else .function @@ -952,15 +943,15 @@ private def getSemanticTokenSyntax (stx : Syntax) : Syntax := | _ => stx private def getAppFnSyntax? (stx : Syntax) : Option Syntax := - if stx.isOfKind ``Parser.Term.app then - some stx[0] - else - none + if stx.isOfKind ``Parser.Term.app then some stx[0] else none private def collectTermInfoBasedSemanticToken (ctx : Elab.ContextInfo) (ti : Elab.TermInfo) : Option LeanSemanticToken := Id.run do let stx := getSemanticTokenSyntax ti.stx if ti.expr.isSort then + unless stx.isOfKind ``Parser.Term.type || stx.isOfKind ``Parser.Term.sort || stx.isOfKind ``Parser.Term.prop do + return none + let stx := stx[0] let .original .. := stx.getHeadInfo | return none return LeanSemanticToken.ofSyntax? stx .class @@ -980,14 +971,19 @@ private def collectTermInfoBasedSemanticToken (ctx : Elab.ContextInfo) (ti : Ela | return none let `($_:ident) := stx | return none + if localDecl.isAuxDecl then + if let some declName := ti.lctx.auxDeclToFullName.get? fvarId then + let env := ctx.cmdEnv?.getD ctx.env + if let some info := env.find? declName then + return LeanSemanticToken.ofSyntax? stx (classifyConstant env info) return (classifyLocal ctx.env ti localDecl).bind (LeanSemanticToken.ofSyntax? stx ·) - | Expr.const declName .. => + | Expr.const declName us => let `($_:ident) := stx | return none let .original .. := stx.getHeadInfo | return none match findConstInfoWithEnv? ctx declName with - | some (env, info) => return LeanSemanticToken.ofSyntax? stx (classifyConstant env declName info ti.expr) + | some (env, info) => return LeanSemanticToken.ofSyntax? stx (classifyConstant env info us) | none => return none | _ => return none diff --git a/tests/server_interactive/semanticTokens.lean b/tests/server_interactive/semanticTokens.lean index 4343eeae8663..a0042c7f9a9a 100644 --- a/tests/server_interactive/semanticTokens.lean +++ b/tests/server_interactive/semanticTokens.lean @@ -1,11 +1,32 @@ /-! This file tests semantic token kinds. -/ -def foo1 (x : Nat) := x.succ -def foo2 (x : Nat) : List Nat := .cons.{0} (x |>.succ) .nil -theorem foo3 (x : Nat) : True := +def dotNotation (x : Nat) := x.succ +def dottedConstructor (x : Nat) : List Nat := .cons.{0} (x |>.succ) .nil +theorem withLocalLet (x : Nat) : True := let y := x.succ .intro +universe u +def TypeAlias := Type + 0 +def SortAlias := Sort (u + 1) +abbrev NatAlias := Nat +def InferredList (α : Type) := List α +def ExplicitList (α : Type) : Type := InferredList α +def singletonNat (x : NatAlias) : ExplicitList NatAlias := [x] + +structure RecursiveStruct where + xs : List RecursiveStruct +class RecursiveClass (α : Type) where + xs : List (RecursiveClass α) + +theorem withHypotheses (p q : Prop) (h1 : p ∧ q) (h2 : p → q) + (h3 : ∀ x : Nat, x = x) : q ∧ 0 = 0 := + ⟨h2 h1.1, h3 0⟩ +theorem withPolymorphicHypothesis (h : ∀ p : Prop, p → p) (f : ∀ α : Type, α → α) : + f Nat 0 = f Nat 0 := + h _ rfl + #eval 1 --^ collectDiagnostics --^ textDocument/semanticTokens/full diff --git a/tests/server_interactive/semanticTokens.lean.out.expected b/tests/server_interactive/semanticTokens.lean.out.expected index e49c645d34c5..3e2b54f83805 100644 --- a/tests/server_interactive/semanticTokens.lean.out.expected +++ b/tests/server_interactive/semanticTokens.lean.out.expected @@ -23,12 +23,33 @@ {"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 5}}, + {"start": {"line": 22, "character": 0}, "end": {"line": 23, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 22, "character": 0}, + "end": {"line": 24, "character": 17}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 25, "character": 0}, "end": {"line": 26, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 25, "character": 0}, + "end": {"line": 27, "character": 9}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 29, "character": 0}, "end": {"line": 29, "character": 5}}, "message": "1", "fullRange": - {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 5}}}]} + {"start": {"line": 29, "character": 0}, + "end": {"line": 29, "character": 5}}}]} {"textDocument": {"uri": "file:///semanticTokens.lean"}, - "position": {"line": 8, "character": 2}} + "position": {"line": 29, "character": 2}} {"data": [0, 4, @@ -42,11 +63,11 @@ 0, 0, 4, - 4, + 11, 3, 0, 0, - 6, + 13, 1, 11, 0, @@ -72,11 +93,11 @@ 0, 0, 4, - 4, + 17, 3, 0, 0, - 6, + 19, 1, 11, 0, @@ -122,11 +143,11 @@ 0, 0, 8, - 4, + 12, 3, 0, 0, - 6, + 14, 1, 11, 0, @@ -167,6 +188,426 @@ 0, 2, 0, + 8, + 0, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 9, + 5, + 0, + 0, + 13, + 4, + 6, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 9, + 5, + 0, + 0, + 13, + 4, + 6, + 0, + 1, + 0, + 6, + 0, + 0, + 0, + 7, + 8, + 5, + 0, + 0, + 12, + 3, + 5, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 12, + 5, + 0, + 0, + 14, + 1, + 10, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 9, + 4, + 5, + 0, + 0, + 5, + 1, + 10, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 12, + 5, + 0, + 0, + 14, + 1, + 10, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 8, + 4, + 6, + 0, + 0, + 8, + 12, + 5, + 0, + 0, + 13, + 1, + 10, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 12, + 3, + 0, + 0, + 14, + 1, + 11, + 0, + 0, + 4, + 8, + 5, + 0, + 0, + 12, + 12, + 5, + 0, + 0, + 13, + 8, + 5, + 0, + 0, + 13, + 1, + 1, + 0, + 2, + 0, + 9, + 0, + 0, + 0, + 10, + 15, + 9, + 0, + 0, + 16, + 5, + 0, + 0, + 1, + 2, + 2, + 2, + 0, + 0, + 5, + 4, + 5, + 0, + 0, + 5, + 15, + 9, + 0, + 1, + 0, + 5, + 0, + 0, + 0, + 6, + 14, + 8, + 0, + 0, + 16, + 1, + 10, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 6, + 5, + 0, + 0, + 1, + 2, + 2, + 2, + 0, + 0, + 5, + 4, + 5, + 0, + 0, + 6, + 14, + 8, + 0, + 0, + 15, + 1, + 10, + 0, + 2, + 0, + 7, + 0, + 0, + 0, + 8, + 14, + 3, + 0, + 0, + 16, + 1, + 7, + 0, + 0, + 2, + 1, + 7, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 7, + 2, + 1, + 0, + 0, + 5, + 1, + 7, + 0, + 0, + 4, + 1, + 7, + 0, + 0, + 4, + 2, + 1, + 0, + 0, + 5, + 1, + 7, + 0, + 0, + 4, + 1, + 7, + 0, + 1, + 5, + 2, + 1, + 0, + 0, + 7, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 5, + 1, + 1, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 5, + 1, + 7, + 0, + 1, + 3, + 2, + 1, + 0, + 0, + 3, + 2, + 1, + 0, + 0, + 6, + 2, + 1, + 0, + 1, + 0, + 7, + 0, + 0, + 0, + 8, + 25, + 3, + 0, + 0, + 27, + 1, + 1, + 0, + 0, + 6, + 1, + 7, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 6, + 1, + 7, + 0, + 0, + 4, + 1, + 7, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 6, + 1, + 10, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 6, + 1, + 10, + 0, + 0, + 4, + 1, + 10, + 0, + 1, + 4, + 1, + 1, + 0, + 0, + 2, + 3, + 5, + 0, + 0, + 8, + 1, + 1, + 0, + 0, + 2, + 3, + 5, + 0, + 1, + 2, + 1, + 1, + 0, + 0, + 2, + 1, + 0, + 0, + 0, + 2, + 3, + 3, + 0, + 2, + 0, 5, 0, 0]}