[RIvance]

This PR improves semantic highlighting (addresses #2305) by reusing information already present in the InfoTree and elaboration context.

This PR DOES NOT:

• change any public API
• OR add/modify constructors to existing inductive definitions
• OR change the InfoTree structure.

It also DOES NOT require any change in lean4-vscode 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 / universe-valued identifiers, e.g. Type, Sort	class
Type parameters, e.g. (A : Type) and uses of A	typeParameter
Typeclass declarations	interface
Structures / records	struct
Propositions and proposition families, e.g. P : Prop, P : A → Prop	enum
Type constructors and type families, e.g. T : Type, F : A → Type	type
Ordinary inductive datatypes	type
Inductive propositions / prop families	enum
Constructors	enumMember
Projection fields and projection functions	property
Term-level definitions, theorems, axioms, opaque declarations, recursors that are not type/proposition families	function
Term-level local binders, e.g. (x : Nat)	parameter
Term-level local uses / proof hypotheses not classified above	variable
Keywords, strings, numbers, Verso doc tokens, sorry-like tokens	keep existing behavior

The PR also handles declaration names and self-references while the declaration is still being elaborated, including recursive function calls and inductive self-references in constructor types.

Closes #2305

AI Usage: I acknowledge the use of Codex GPT-5.5 for assistance in coding, code review, and test case generation.

LHS: With Semantic Highlighting; RHS: Without Semantic Highlighting

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bba3868b3b1dfd7741d33b119f73b5d342b9f1d5 --onto ed0d50fcf0efa8c9a32e1ccb3603ce43edce6926. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-13 16:31:23)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2acdaafcfe34015fba2490e68600d5c4585f5a47 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-15 11:08:32)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1b8f1f140c56d214b2171abe8675fb8582670fef --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-16 08:48:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 50e882b0dff5001d7dc1320f91c3fbcb610aad31 --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-02 09:20:54)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bba3868b3b1dfd7741d33b119f73b5d342b9f1d5 --onto ed0d50fcf0efa8c9a32e1ccb3603ce43edce6926. You can force reference manual CI using the force-manual-ci label. (2026-05-13 16:31:26)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2acdaafcfe34015fba2490e68600d5c4585f5a47 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-15 11:08:34)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1b8f1f140c56d214b2171abe8675fb8582670fef --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-16 08:48:56)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 50e882b0dff5001d7dc1320f91c3fbcb610aad31 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-02 09:20:55)

[RIvance]

closing this in favor of #16151 with RFC #16150