From dee5a4ed7110a055922cb3c94ff7087a19b47d58 Mon Sep 17 00:00:00 2001 From: ivance Date: Wed, 13 May 2026 16:07:12 +0800 Subject: [PATCH 1/3] feat: improve semantic highlighting --- .../FileWorker/SemanticHighlighting.lean | 115 ++- tests/server_interactive/semanticTokens.lean | 37 + .../semanticTokens.lean.out.expected | 652 +++++++++++++++++- 3 files changed, 770 insertions(+), 34 deletions(-) diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index dbfe4cbe254b..cf7019dfa11a 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -492,25 +492,110 @@ partial def collectSyntaxBasedSemanticTokens (text : FileMap) : (stx : Syntax) return tokens return tokens.push { stx, type := 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 + -- Recall that `isAuxDecl` is an auxiliary declaration used to elaborate a recursive definition. + if localDecl.isAuxDecl then + if ti.isBinder then + return some .function + else + return none + if localDecl.isImplementationDetail then + return none + let localType := localDecl.type + if let some tokenType := typeForSortResult? localType then + if localType.isSort && tokenType == .type then + return some .typeParameter + else + return some tokenType + 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 collectTermInfoBasedSemanticToken (ctx : Elab.ContextInfo) (ti : Elab.TermInfo) : + Option LeanSemanticToken := Id.run do + let .original .. := ti.stx.getHeadInfo + | return none + if ti.expr.isSort then + return some { stx := ti.stx, type := .class } + if ti.stx.getKind == Parser.Term.identProjKind then + return some { stx := ti.stx, type := .property } + if let `($_:ident) := ti.stx then + match ti.expr with + | Expr.fvar fvarId .. => + match ti.lctx.find? fvarId with + | some localDecl => + let tokenType? := classifyLocal ctx.env ti localDecl + return tokenType?.map fun tokenType => ⟨ti.stx, tokenType, 5⟩ + | none => return none + | _ => + match ti.expr.getAppFn with + | Expr.const declName .. => + match ctx.env.find? declName with + | some info => return some ⟨ti.stx, classifyConstant ctx.env declName info ti.expr, 5⟩ + | none => return 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 { stx := ti.stx, type := SemanticTokenType.function } - else if ! localDecl.isImplementationDetail then - return { stx := ti.stx, type := SemanticTokenType.variable } - if ti.stx.getKind == Parser.Term.identProjKind then - return {stx := ti.stx, type := SemanticTokenType.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..7ee7ebe00c50 100644 --- a/tests/server_interactive/semanticTokens.lean +++ b/tests/server_interactive/semanticTokens.lean @@ -1,7 +1,44 @@ +/-! This file tests semantic token kinds. -/ + +universe u + +inductive SemanticTokenData where + | atom : SemanticTokenData + +inductive SemanticTokenProp (A : Type u) : A → Prop where + | intro (a : A) : SemanticTokenProp A a + +structure SemanticTokenStruct where + field : Nat + +class SemanticTokenInterface (A : Type u) where + op : A → A + +def SemanticTokenFamily (A : Type u) : Type u := List A + +def SemanticTokenPredicate (A : Type u) (a : A) : Prop := a = a + +def semanticTokenValue : Nat := 1 + +theorem semanticTokenProof (A : Type u) (a : A) : SemanticTokenPredicate A a := rfl + +def semanticTokenUse (A : Type u) [SemanticTokenInterface A] (a : A) + (h : SemanticTokenProp A a) : SemanticTokenFamily Nat := + let s : SemanticTokenStruct := { field := semanticTokenValue } + let d : SemanticTokenData := SemanticTokenData.atom + let p : SemanticTokenPredicate A a := semanticTokenProof A a + let q : SemanticTokenProp A a := h + match d with + | .atom => + let _ : SemanticTokenPredicate A a := p + let _ : SemanticTokenProp A a := q + List.cons s.field List.nil + def foo1 (x : Nat) := x.succ def foo2 (x : Nat) := x |>.succ theorem foo3 (x : Nat) : True := let y := x.succ + have : y = y := rfl True.intro #eval 1 diff --git a/tests/server_interactive/semanticTokens.lean.out.expected b/tests/server_interactive/semanticTokens.lean.out.expected index 38c8cd057d66..1cfd97ff38d2 100644 --- a/tests/server_interactive/semanticTokens.lean.out.expected +++ b/tests/server_interactive/semanticTokens.lean.out.expected @@ -5,103 +5,717 @@ [{"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 2, "character": 0}, "end": {"line": 3, "character": 0}}, + {"start": {"line": 22, "character": 0}, + "end": {"line": 22, "character": 83}}, "message": "Goals accomplished!", "leanTags": [2], "isSilent": true, "fullRange": - {"start": {"line": 2, "character": 0}, "end": {"line": 4, "character": 12}}}, - {"tags": [1], - "source": "Lean 4", - "severity": 2, + {"start": {"line": 22, "character": 0}, + "end": {"line": 22, "character": 83}}}, + {"source": "Lean 4", + "severity": 3, "range": - {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}, - "message": - "unused variable `y`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`", + {"start": {"line": 38, "character": 0}, "end": {"line": 39, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, "fullRange": - {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}}, + {"start": {"line": 38, "character": 0}, + "end": {"line": 41, "character": 12}}}, {"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 5}}, + {"start": {"line": 43, "character": 0}, "end": {"line": 43, "character": 5}}, "message": "1", "fullRange": - {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 5}}}]} + {"start": {"line": 43, "character": 0}, + "end": {"line": 43, "character": 5}}}]} {"textDocument": {"uri": "file:///semanticTokens.lean"}, - "position": {"line": 6, "character": 2}} + "position": {"line": 43, "character": 2}} {"data": - [0, + [2, 0, - 3, + 8, 0, 0, + 2, 0, - 10, + 9, + 0, + 0, + 0, + 28, + 5, + 0, + 0, + 1, + 4, + 4, + 12, + 0, + 2, + 0, + 9, + 0, + 0, + 0, + 29, 1, + 10, + 0, + 0, + 4, + 6, + 6, + 0, + 0, + 10, 1, + 10, 0, 0, + 4, + 4, + 6, + 0, + 0, + 5, + 5, + 0, + 0, + 1, + 4, + 5, 12, + 0, + 0, + 7, + 1, + 11, + 0, + 0, + 4, + 1, + 10, + 0, + 0, + 23, + 1, + 10, + 0, + 0, + 2, + 1, 1, + 0, + 2, + 0, + 9, + 0, + 0, + 0, + 30, + 5, + 0, + 0, 1, + 2, + 5, + 2, 0, 0, + 8, + 3, + 5, + 0, 2, + 0, + 5, + 0, + 0, + 0, + 30, + 1, + 10, + 0, + 0, 4, + 6, + 6, + 0, + 0, + 8, + 5, + 0, + 0, + 1, + 2, + 2, 2, 0, + 0, + 5, + 1, + 10, + 0, + 0, + 4, 1, + 10, + 0, + 2, 0, 3, 0, 0, 0, + 4, + 19, + 5, + 0, + 0, + 21, + 1, + 10, + 0, + 0, + 4, + 6, + 6, + 0, + 0, + 10, + 6, + 6, + 0, + 0, 10, + 4, + 5, + 0, + 0, + 5, 1, + 10, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 22, + 7, + 0, + 0, + 24, 1, + 10, 0, 0, - 12, + 4, + 6, + 6, + 0, + 0, + 9, 1, + 11, + 0, + 0, + 4, 1, + 10, 0, 0, 5, 4, - 2, + 6, + 0, 0, + 8, 1, + 1, + 0, + 0, + 4, + 1, + 1, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 18, + 3, + 0, + 0, + 21, + 3, + 5, + 0, + 2, 0, 7, 0, 0, 0, - 14, + 8, + 18, + 3, + 0, + 0, + 20, + 1, + 10, + 0, + 0, + 4, + 6, + 6, + 0, + 0, + 9, + 1, + 11, + 0, + 0, + 4, 1, + 10, + 0, + 0, + 5, + 22, + 7, + 0, + 0, + 23, 1, + 10, + 0, 0, + 2, + 1, 1, + 0, + 0, + 5, + 3, + 3, + 0, 2, + 0, + 3, + 0, + 0, + 0, + 4, + 16, 3, 0, 0, + 18, + 1, + 10, + 0, 0, 4, + 6, + 6, + 0, + 0, + 9, + 22, + 8, + 0, + 0, + 23, 1, + 10, + 0, + 0, + 4, 1, + 11, + 0, 0, + 4, + 1, + 10, 0, + 1, 5, 1, 1, 0, 0, - 2, 4, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 19, + 5, + 0, + 0, + 20, + 3, + 5, + 0, + 1, 2, + 3, 0, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 4, + 19, + 9, + 0, + 0, + 34, + 18, + 3, + 0, + 1, + 2, 3, 0, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 4, + 17, + 5, + 0, + 0, + 21, + 22, + 12, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 4, + 22, + 7, + 0, + 0, + 23, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 18, + 3, + 0, + 0, + 19, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 4, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 1, + 1, + 0, + 1, + 2, + 5, + 0, + 0, + 0, + 6, + 1, + 1, + 0, + 0, + 2, + 4, + 0, + 0, + 2, + 4, + 3, + 0, + 0, + 0, + 4, + 1, + 0, + 0, + 0, + 4, + 22, + 7, + 0, + 0, + 23, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 1, + 1, + 0, + 1, + 4, + 3, + 0, + 0, + 0, + 4, + 1, + 0, + 0, + 0, + 4, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 1, + 1, + 0, + 1, + 4, + 9, + 12, + 0, + 0, + 10, + 1, + 1, + 0, + 0, + 2, + 5, + 2, + 0, + 0, + 6, + 8, + 12, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 4, + 3, + 0, + 0, + 6, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 8, + 1, + 1, + 0, + 0, + 2, + 4, + 2, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 4, + 3, + 0, + 0, + 6, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 8, + 1, + 1, + 0, + 0, + 5, + 4, + 2, + 0, + 1, + 0, + 7, + 0, + 0, + 0, + 8, + 4, + 3, + 0, + 0, + 6, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 7, + 4, + 7, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 5, + 1, + 1, + 0, + 0, + 2, + 4, + 2, + 0, + 1, + 2, + 4, + 0, + 0, + 0, + 7, + 1, + 1, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 5, + 3, + 3, + 0, + 1, + 2, + 10, + 12, + 0, + 2, + 0, 5, 0, 0]} From a7710f415cca6f4ffa63ec9f3e2718eddf50fc4c Mon Sep 17 00:00:00 2001 From: ivance Date: Wed, 13 May 2026 18:06:06 +0800 Subject: [PATCH 2/3] fix: semantic highlighting for recursive definition --- .../FileWorker/SemanticHighlighting.lean | 87 +++++++++++------ tests/server_interactive/semanticTokens.lean | 4 + .../semanticTokens.lean.out.expected | 97 ++++++++++++++++--- 3 files changed, 144 insertions(+), 44 deletions(-) diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index cf7019dfa11a..3dd9d6024f5b 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -523,20 +523,21 @@ private partial def typeExprResult? (env : Environment) (lctx : LocalContext) (t private def classifyLocal (env : Environment) (ti : Elab.TermInfo) (localDecl : LocalDecl) : Option SemanticTokenType := Id.run do - -- Recall that `isAuxDecl` is an auxiliary declaration used to elaborate a recursive definition. + 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 ti.isBinder then - return some .function + if let some tokenType := typeForSortResult? localType then + return some tokenType else - return none - if localDecl.isImplementationDetail then - return none - let localType := localDecl.type + 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 @@ -565,30 +566,60 @@ private def classifyConstant (env : Environment) (declName : Name) (info : Const 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 := + match stx with + | `(Parser.Command.declId|$id$[.{$_ls,*}]?) => 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 .original .. := ti.stx.getHeadInfo - | return none + let stx := getSemanticTokenSyntax ti.stx if ti.expr.isSort then - return some { stx := ti.stx, type := .class } - if ti.stx.getKind == Parser.Term.identProjKind then - return some { stx := ti.stx, type := .property } - if let `($_:ident) := ti.stx then - match ti.expr with - | Expr.fvar fvarId .. => - match ti.lctx.find? fvarId with - | some localDecl => - let tokenType? := classifyLocal ctx.env ti localDecl - return tokenType?.map fun tokenType => ⟨ti.stx, tokenType, 5⟩ - | none => return none - | _ => - match ti.expr.getAppFn with - | Expr.const declName .. => - match ctx.env.find? declName with - | some info => return some ⟨ti.stx, classifyConstant ctx.env declName info ti.expr, 5⟩ - | none => return none - | _ => return none - return none + let .original .. := stx.getHeadInfo + | return none + return some { stx, type := .class } + if stx.getKind == Parser.Term.identProjKind then + let .original .. := stx.getHeadInfo + | return none + return some { stx, type := .property } + 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).map fun tokenType => ⟨stx, tokenType, 5⟩ + | Expr.const declName .. => + let `($_:ident) := stx + | return none + let .original .. := stx.getHeadInfo + | return none + match findConstInfoWithEnv? ctx declName with + | some (env, info) => return some ⟨stx, classifyConstant env declName info ti.expr, 5⟩ + | none => return none + | _ => return none /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken := diff --git a/tests/server_interactive/semanticTokens.lean b/tests/server_interactive/semanticTokens.lean index 7ee7ebe00c50..e26d970bfe53 100644 --- a/tests/server_interactive/semanticTokens.lean +++ b/tests/server_interactive/semanticTokens.lean @@ -20,6 +20,10 @@ def SemanticTokenPredicate (A : Type u) (a : A) : Prop := a = a def semanticTokenValue : Nat := 1 +def semanticTokenRecursive : Nat → Nat + | 0 => 0 + | n + 1 => semanticTokenRecursive n + theorem semanticTokenProof (A : Type u) (a : A) : SemanticTokenPredicate A a := rfl def semanticTokenUse (A : Type u) [SemanticTokenInterface A] (a : A) diff --git a/tests/server_interactive/semanticTokens.lean.out.expected b/tests/server_interactive/semanticTokens.lean.out.expected index 1cfd97ff38d2..fd125dcf50a9 100644 --- a/tests/server_interactive/semanticTokens.lean.out.expected +++ b/tests/server_interactive/semanticTokens.lean.out.expected @@ -5,34 +5,34 @@ [{"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 22, "character": 0}, - "end": {"line": 22, "character": 83}}, + {"start": {"line": 26, "character": 0}, + "end": {"line": 26, "character": 83}}, "message": "Goals accomplished!", "leanTags": [2], "isSilent": true, "fullRange": - {"start": {"line": 22, "character": 0}, - "end": {"line": 22, "character": 83}}}, + {"start": {"line": 26, "character": 0}, + "end": {"line": 26, "character": 83}}}, {"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 38, "character": 0}, "end": {"line": 39, "character": 0}}, + {"start": {"line": 42, "character": 0}, "end": {"line": 43, "character": 0}}, "message": "Goals accomplished!", "leanTags": [2], "isSilent": true, "fullRange": - {"start": {"line": 38, "character": 0}, - "end": {"line": 41, "character": 12}}}, + {"start": {"line": 42, "character": 0}, + "end": {"line": 45, "character": 12}}}, {"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 43, "character": 0}, "end": {"line": 43, "character": 5}}, + {"start": {"line": 47, "character": 0}, "end": {"line": 47, "character": 5}}, "message": "1", "fullRange": - {"start": {"line": 43, "character": 0}, - "end": {"line": 43, "character": 5}}}]} + {"start": {"line": 47, "character": 0}, + "end": {"line": 47, "character": 5}}}]} {"textDocument": {"uri": "file:///semanticTokens.lean"}, - "position": {"line": 43, "character": 2}} + "position": {"line": 47, "character": 2}} {"data": [2, 0, @@ -45,7 +45,12 @@ 0, 0, 0, - 28, + 10, + 17, + 5, + 0, + 0, + 18, 5, 0, 0, @@ -54,13 +59,23 @@ 4, 12, 0, + 0, + 7, + 17, + 5, + 0, 2, 0, 9, 0, 0, 0, - 29, + 10, + 17, + 7, + 0, + 0, + 19, 1, 10, 0, @@ -100,7 +115,12 @@ 10, 0, 0, - 23, + 5, + 17, + 7, + 0, + 0, + 18, 1, 10, 0, @@ -115,7 +135,12 @@ 0, 0, 0, - 30, + 10, + 19, + 9, + 0, + 0, + 20, 5, 0, 0, @@ -135,7 +160,12 @@ 0, 0, 0, - 30, + 6, + 22, + 8, + 0, + 0, + 24, 1, 10, 0, @@ -261,6 +291,41 @@ 0, 2, 0, + 3, + 0, + 0, + 0, + 4, + 22, + 3, + 0, + 0, + 25, + 3, + 5, + 0, + 0, + 6, + 3, + 5, + 0, + 2, + 4, + 1, + 11, + 0, + 0, + 9, + 22, + 3, + 0, + 0, + 23, + 1, + 1, + 0, + 2, + 0, 7, 0, 0, From 7b485cea1d96eb4bbb3267dce9cf0c678f82ef6d Mon Sep 17 00:00:00 2001 From: ivance Date: Thu, 14 May 2026 01:13:14 +0800 Subject: [PATCH 3/3] fix: test failure on tests/server_interactive/semanticTokensVersoDocs.lean --- .../semanticTokensVersoDocs.lean.out.expected | 114 +++++++++++++++--- 1 file changed, 97 insertions(+), 17 deletions(-) diff --git a/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected b/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected index 236c9a2f483b..81a695a2f663 100644 --- a/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected +++ b/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected @@ -68,7 +68,7 @@ 0, 1, 4, - 18, + 3, 0, 0, 4, @@ -97,11 +97,16 @@ 0, 0, 1, - 5, + 4, + 3, + 0, + 0, + 4, + 1, 18, 0, 0, - 5, + 1, 1, 1, 0, @@ -132,11 +137,16 @@ 0, 0, 1, - 10, + 4, + 3, + 0, + 0, + 4, + 6, 18, 0, 0, - 10, + 6, 1, 0, 0, @@ -146,12 +156,22 @@ 0, 0, 0, - 10, + 4, + 4, + 3, + 0, + 0, + 6, 1, 1, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, @@ -183,7 +203,7 @@ 0, 1, 4, - 18, + 3, 0, 0, 4, @@ -212,11 +232,16 @@ 0, 0, 1, - 5, + 4, + 3, + 0, + 0, + 4, + 1, 18, 0, 0, - 5, + 1, 1, 1, 0, @@ -247,11 +272,21 @@ 0, 0, 1, - 11, + 4, + 3, + 0, + 0, + 4, + 3, 18, 0, 0, - 11, + 3, + 4, + 3, + 0, + 0, + 4, 1, 0, 0, @@ -261,12 +296,22 @@ 0, 0, 0, - 10, + 4, + 4, + 3, + 0, + 0, + 6, 1, 1, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, @@ -357,21 +402,51 @@ 0, 1, 0, + 10, 18, - 18, 0, 0, + 10, + 3, + 3, + 0, + 0, + 3, + 5, 18, + 0, + 0, + 5, 1, + 11, + 0, + 0, 1, + 3, + 18, + 0, + 0, + 3, + 4, + 5, + 0, 0, + 4, + 2, + 18, 0, + 0, + 2, 1, - 13, + 3, + 0, + 0, + 1, + 3, 18, 0, 0, - 13, + 3, 1, 1, 0, @@ -504,4 +579,9 @@ 0, 3, 0, + 0, + 0, + 4, + 1, + 3, 0]}