feat: inlay hints for auto-implicits

[mhuisi]

This PR adds preliminary support for inlay hints, as well as support for inlay hints that denote the auto-implicits of a function. Hovering over an auto-implicit displays its type and double-clicking the auto-implicit inserts it into the text document.

This PR is an extension of #3910.

Known issues

• In VS Code, when inserting an inlay hint, the inlay hint may linger for a couple of seconds before it disappears. This is a defect of the VS Code implementation of inlay hints and cannot adequately be resolved by us.
• When making a change to the document, it may take a couple of seconds until the inlay hints respond to the change. This is deliberate and intended to reduce the amount of inlay hint flickering while typing. VS Code has a mechanism of its own for this, but in my experience it is still far too sensitive without additional latency.
• Inserting an auto-implicit inlay hint that depends on an auto-implicit meta-variable causes a "failed to infer binder type" error. We can't display these meta-variables in the inlay hint because they don't have a user-displayable name, so it is not clear how to resolve this problem.
• Inlay hints are currently always resolved eagerly, i.e. we do not support the textDocument/inlayHint/resolve request yet. Implementing support for this request is future work.

Other changes

• Axioms did not support auto-implicits due to an oversight in the implementation. This PR ensures they do.
• In order to reduce the amount of inlay hint flickering when making a change to the document, the language server serves old inlay hints for parts of the file that have not been processed yet. This requires LSP request handler state (that sometimes must be invalidated on textDocument/didChange), so this PR introduces the notion of a stateful LSP request handler.
• The partial response mechanism that we use for semantic tokens, where we simulate incremental LSP responses by periodically emitting refresh requests to the client, is generalized to accommodate both inlay hints and semantic tokens. Additionally, it is made more robust to ensure that we never emit refresh requests while a corresponding request is in flight, which causes VS Code to discard the respond of the request, as well as to ensure that we keep prompting VS Code to send another request if it spuriously decides not to respond to one of our refresh requests.
• The synthetic identifier of an example had the full declaration as its (non-canonical synthetic) range. Since we need a reasonable position for the identifier to insert an inlay hint for the auto-implicits of an example, we change the (canonical synthetic) range of the synthetic identifier to that of the example keyword.
• The semantic highlighting request handling is moved to a separate file.

Breaking changes

• The semantic highlighting request handler is not a pure request handler anymore, but a stateful one. Notably, this means that clients that extend the semantic highlighting of the Lean language server with the chainLspRequestHandler function must now use the chainStatefulLspRequestHandler function instead.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c07f64a6212247ef789d4cef39e237b4a4b61696 --onto c70f4064b4041dee70925bddbef095ebb2b36d7d. (2025-01-24 17:38:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c07f64a6212247ef789d4cef39e237b4a4b61696 --onto 832d7c500d709deb5e7f0a5a6fd0f01865d1a303. (2025-02-03 15:28:25)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c07f64a6212247ef789d4cef39e237b4a4b61696 --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-04 16:46:15)