feat: snippet extension

[Vtec234]

Summary

This makes a small addition to our take on the LSP protocol
in the form of supporting snippet text edits.
It has been discussed here on the LSP issue tracker for a while,
but seems unlikely to be added anytime soon.
This feature was requested by @PatrickMassot for the purposes
of supporting Lean code templates in code actions and widgets.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-12 21:26:34)
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-20' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-20 09:31:22)

[PatrickMassot]

The LSP issue isn't easy to read, so let me quote it. The main point is here:

we decided that we only add something to the spec if we have an implementation in a client. Otherwise things are hard to spec and to get feedback on.

You would think the process is: 1) add some feature to the LSP spec 2) get this feature implemented in editors. But the comment above proves it goes the other way around. So indeed "insert snippets as text edits" is not yet part of the LSP specification but it is already supported by VSCode.

[david-christiansen]

@PatrickMassot Requiring implementations before adding something to a spec is very good practice - it's difficult to know what will be good in practice without having first used it. IMHO they should require at least two completely independent implementations - this would also help discover places where the documentation or specification is lacking and help ensure that the protocol actually does meet its goal of working in multiple editors.

[david-christiansen]

I have some stylistic nitpicks on docstrings.

I can think of lots of cases where this would be a really nice feature!

[PatrickMassot]

@PatrickMassot Requiring implementations before adding something to a spec is very good practice - it's difficult to know what will be good in practice without having first used it. IMHO they should require at least two completely independent implementations - this would also help discover places where the documentation or specification is lacking and help ensure that the protocol actually does meet its goal of working in multiple editors.

I'm not complaining at all, I'm was trying to provide more context in order to avoid seeing this important PR closed by someone arguing this isn't part of the spec.

[mhuisi]

Very late approval, but these changes look good to me.