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

[Dmitry Gutov <dmitry@gutov.dev>]

Cc'ing Joao.

On 15/10/2023 05:24, Richard Copley 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?
> 
> 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)