feat: show declaration keywords in hovers

[david-christiansen]

This PR adds declaration keywords, such as def or class, to signatures in hovers.

Declaration keywords are now shown in hovers as part of a signature. This is in support of an upcoming documentation style guide that will recommend that the text of docstrings not state what sort of declaration something is, but instead leave it to Lean to tell every user in a consistent manner.

Screenshot:

[david-christiansen]

In most cases, this didn't require much work. However, the name of a class, structure, or class inductive in the declaration itself is saved to the infotree using an environment in which the structure info or class info is not yet present. To make these hovers correct, hovers on names of inductive types also check whether the occurrence in question is such an occurrence, and then uses the containing declaration as a source for the keyword.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-7232 has successfully built against this PR. (2025-02-26 00:46:23) View Log

[mhuisi]

I'd love to have this feature, but I am a bit concerned about the lack of extensibility by the approach in this PR. For example, in Mathlib, hovering over a lemma will display as theorem, which isn't great.

Should we instead thread this information through to the language server, e.g. as a separate environment extension (e.g. as for DeclarationRanges, with a MapDeclarationExtension)?