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?
Here is an example request and reply. The reply is cut down from an
original list of over 200 suggestions.
[client-request]
(:jsonrpc "2.0" :id 777 :method "textDocument/codeAction" :params
(:textDocument
(:uri"file:///s%3A/projects/lean/float/Fl/Lemmas.lean") :range
(:start (:line 50 :character 2) :end (:line 50 :character 8))
:context (:diagnostics [])))
[server-reply]
(:result
[(:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
(:documentChanges
[(:textDocument
(:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
:edits
[(:range
(:start (:line 50 :character 2) :end (:line 50 :character 8))
:newText "refine Nat.add_left_cancel ?_")])]
:changes nil :changeAnnotations nil))
(:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
(:documentChanges
[(:textDocument
(:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
:edits
[(:range
(:start (:line 50 :character 2) :end (:line 50 :character 8))
:newText "refine Nat.add_right_cancel ?_")])]
:changes nil :changeAnnotations nil))
(:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
(:documentChanges
[(:textDocument
(:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
:edits
[(:range
(:start (:line 50 :character 2) :end (:line 50 :character 8))
:newText "refine Nat.eq_of_mul_eq_mul_right ?_")])]
:changes nil :changeAnnotations nil))
(:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
(:documentChanges
[(:textDocument
(:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
:edits
[(:range
(:start (:line 50 :character 2) :end (:line 50 :character 8))
:newText "refine Nat.eq_of_mul_eq_mul_left ?_")])]
:changes nil :changeAnnotations nil))]
:jsonrpc "2.0" :id 777)