[RIvance]

This PR improves semantic highlighting (RFC #16150).

It reuses information already present in the InfoTree and elaboration context.

This PR does not:

• change any public API
• add or modify constructors of existing inductive definitions
• change the InfoTree structure

It also requires no changes to the Lean VS Code extension because the server still emits standard semantic token types from the existing SemanticTokenType. No new token kinds are introduced, so existing VS Code themes should continue to work.

The mapping is:

Lean entity	Token type
Universe expressions and universe-valued identifiers, e.g. Type, Sort	class
Type parameters and their uses, e.g. (A : Type) and uses of A	typeParameter
Typeclass declarations	interface
Structures and records	struct
Propositions and proposition families, including inductive ones, e.g. P : Prop, P : A → Prop	enum
Type constructors, type families, and ordinary inductive datatypes, e.g. T : Type, F : A → Type	type
Constructors	enumMember
Projection fields and projection functions	property
Term-level definitions, theorems, axioms, opaque declarations, and recursors, excluding type/proposition families	function
Local term binders, e.g. (x : Nat)	parameter
Local term uses and proof hypotheses not classified above	variable
Keywords, strings, numbers, Verso doc tokens, and sorry-like tokens	Existing behavior

RFC: #16150

Closes #2305 #16150

AI Usage: I acknowledge the use of Codex for assistance with coding, code review, and tests. All changes are reviewed by human.

LHS: With Semantic Highlighting; RHS: Without Semantic Highlighting

[RIvance]

changelog-server

[matthiasgoergens]

Thanks for working on this, the classification is a useful addition. Below are four cases that come out wrong.

All four reproducers can be run the same way: save the snippet as tests/server_interactive/x.lean, append the three lines #eval 1, --^ collectDiagnostics and --^ textDocument/semanticTokens/full as in semanticTokens.lean, put the bin directory of the pr-release-16151 toolchain on PATH, and run cd tests/server_interactive && lean -Dlinter.all=false --run run_test.lean x.lean. The data array in the output is the standard LSP delta encoding; the tables below are decoded (line numbers start at 1, columns at 0, lengths in UTF-16 units).

1. The class token for a sort covers the whole Type .../Sort ... expression, not only its leading keyword.

universe u v
example : Type 1 := Type
  0
example : Type 1 := Type
                                 0
example : Sort (max u v + 1) := Sort (max u v)

where	actual	expected
line 2, col 20	class, length 0	class, length 4 (Type)
line 4, col 20	class, length 14 (the line has 24 characters)	class, length 4 (Type)
line 6, cols 10-27 (Sort (max u v + 1))	Sort keyword, ( class, max keyword, u v + 1) class	Sort as class; no class token on the level arguments

When the expression spans two lines, the length is computed in computeDeltaLspSemanticTokens (src/Lean/Server/FileWorker/SemanticHighlighting.lean) as the difference of the end and start columns, which gives 0 or a length past the end of the line. Both symptoms and the level-argument case disappear if the token covers only the leading atom. Could you emit the sort token for the leading Type/Sort/Prop atom only?

2. Type-valued definitions without a type annotation are function at the declaration and type at every use.

def MyNat := Nat
abbrev N := Nat
def F (α : Type) := List α
def G (α : Type) : Type := List α
example (a : MyNat) (b : N) (c : F Nat) (d : G Nat) : Nat := 0

name	declaration (lines 1-4)	use (line 5)	expected
MyNat	function	type	type
N	function	type	type
F	function	type	type
G	type	type	type

The description lists type constructors and type families as type and excludes them from function, and G shows that declarations with a written type already follow that. In classifyLocal the isAuxDecl branch returns .function when the declared type is not already a sort, which is the case when the type is inferred. Could you classify the declaration name of such a definition as type, as at its uses?

3. A structure or class mentioned inside its own declaration is type, not struct/interface.

structure Node where
  children : List Node
class Cl (α : Type) where
  d : List (Cl α)

position	actual	expected
line 1, col 10 (Node, declaration)	struct	struct
line 2, col 18 (Node in List Node)	type	struct
line 3, col 6 (Cl, declaration)	interface	interface
line 4, col 12 (Cl in List (Cl α))	type	interface

Inside its own declaration the name is a local auxiliary declaration, and the isAuxDecl branch of classifyLocal only looks at its type, not at isStructure/isClass. Could you consult those for auxiliary declarations too?

4. Hypotheses whose type is an implication or a ∀ are parameter at the binder; other hypotheses are variable.

theorem t (P Q : Prop) (h1 : P ∧ Q) (h2 : P → Q) (h3 : ∀ n : Nat, n = n) : True := .intro

binder	actual	expected
h1 (col 24)	variable	variable
h2 (col 37)	parameter	variable
h3 (col 50)	parameter	variable

The description maps proof hypotheses to variable, and h1 follows that. typeExprResult? looks at the head of the type without first stripping the leading binders, so an implication or ∀ matches nothing and falls through to parameter. Could you apply forallBody to the type before that lookup?

Tested on Linux x86_64 with the pr-release-16151 toolchain (Lean 4.37.0-pre, commit 392ff24; src/Lean/Server is identical at the current head).

[Kha]

Thanks for working on this, the classification is a useful addition.

@matthiasgoergens Could I ask you not to phrase comments in such a way that they could be understood as official reviews?

[RIvance]

@matthiasgoergens Thanks a lot for your review! I agree that the points you raised are genuine inconsistencies that needed to be addressed and I appreciate you pointing them out. They have now been fixed.