bug#66552: 30.0.50; Eglot feature request: handle quirky code actions

["João Távora" <joaotavora@gmail.com>]

On Sun, Oct 15, 2023 at 3:25 AM Richard Copley <rcopley@gmail.com> wrote:
>
> The language server for Lean 4 [1] provides code actions with a couple
> of features that make it difficult to apply them from within Eglot.
>
> [1] https://github.com/leanprover/lean4
>
> Firstly, the textDocument version field has the value 0, which is
> generally not equal to the version in `eglot--versioned-identifier',
> resulting in the error "Edits on `%s' require version %d, you have %d"
> from `eglot--apply-text-edits'.
>
> Secondly, all the suggestions have the same title ("Apply 'Try this'"),
> which means an alist using the title as the key can't be used in
> completing-read as in `eglot--read-execute-code-action'.
>
> Could you provide options to ignore the version, and to use the newText
>  (JSONPath $.result[:1].edit.documentChanges[:1].edits[:1].newText)
> instead of the title?

I understand the problem, thanks for describing it nicely.

Anyway, I don't think patching this in a client like Eglot is
recommended.  Both these thinks are bugs in the language server
and should be fixed there.  Eglot is an LSP client which works
with tens, maybe hundreds, of servers, it can't bloat itself
to work around every server's quirks.

For the version field, servers don't _have_ to send one (if I
remember correctly).  If a servers sends no field, Eglot will
ignore it.  If it sends a wrong one, Eglot won't.

You could work around it with a monkey-patch by advising
eglot--apply-text-edits to always have a null second argument.

The second labeling problem is even more bizarre  Again, you
can probably monkey-patch Eglot to work around it.

But I really think you should report these two things to the
language server authors.

João