feat: inlay hint refinements

[mhuisi]

This PR implements a number of refinements for the auto-implicit inlay hints implemented in #6768.
Specifically:

• In feat: inlay hints for auto-implicits #6768, there was a bug where the inlay hint edit delay could accumulate on successive edits, which meant that it could sometimes take much longer for inlay hints to show up. This PR implements the basic infrastructure for request cancellation and implements request cancellation for semantic tokens and inlay hints to resolve the issue. With this edit delay bug fixed, it made more sense to increase the edit delay slightly from 2000ms to 3000ms.
• In feat: inlay hints for auto-implicits #6768, we applied the edit delay to every single inlay hint request in order to reduce the amount of inlay hint flickering. This meant that the edit delay also had a significant effect on how far inlay hints would lag behind the file progress bar. This PR adjusts the edit delay logic so that it only affects requests sent directly after a corresponding didChange notification. Once the edit delay is used up, all further semantic token requests are responded to without delay, so that the only latency that affects how far the inlay hints lag behind the progress bar is how often we emit refresh requests and how long VS Code takes to respond to them.
• For inlay hints, refresh requests are now emitted 500ms after a response to an inlay hint request, not 2000ms, which means that after the edit delay, inlay hints should only lag behind the progress bar by about up to 500ms. This is justifiable for inlay hints because the response should be much smaller than e.g. is the case for semantic tokens.
• In feat: inlay hints for auto-implicits #6768, 'Restart File' did not prompt a refresh, but it does now.
• VS Code does not immediately remove old inlay hints from the document when they are applied. In feat: inlay hints for auto-implicits #6768, this meant that inlay hints would linger around for a bit once applied. To mitigate this issue, this PR adjusts the inlay hint edit delay logic to identify edits sent from the client as being inlay hint applications, and sets the edit delay to 0ms for the inlay hint requests following it. This means that inlay hints are now applied immediately.
• In feat: inlay hints for auto-implicits #6768, hovering over single-letter auto-implicit inlay hints was a bit finicky because VS Code uses the regular cursor icon on inlay hints, not the thin text cursor icon, which means that it is easy to put the cursor in the wrong spot. We now add the separation character ( or {) preceding an auto-implicit to the hover range as well, which makes hovering over inlay hints much smoother.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-05 19:37:36)
• ✅ Mathlib branch lean-pr-testing-6959 has successfully built against this PR. (2025-02-06 17:25:33) View Log