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

[Richard Copley]

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)



In GNU Emacs 30.0.50 (build 1, x86_64-w64-mingw32) of 2023-10-12 built
 on MACHINE
Repository revision: 90b4a7acb5332ed490cb2b456cfe8c11af8c9d4f
Repository branch: master
Windowing system distributor 'Microsoft Corp.', version 10.0.19045
System Description: Microsoft Windows 10 Pro (v10.0.2009.19045.3448)

Configured using:

'configure --config-cache --with-modules --without-pop
--without-compress-install --with-tree-sitter --without-libsystemd
--without-dbus --without-gconf --without-gsettings --without-mailutils
--with-small-ja-dic --with-native-compilation --prefix=/mingw64
--build=x86_64-w64-mingw32

Configured features:
ACL GIF GMP GNUTLS HARFBUZZ JPEG JSON LCMS2 LIBXML2 MODULES NATIVE_COMP
NOTIFY W32NOTIFY PDUMPER PNG RSVG SOUND SQLITE3 THREADS TIFF
TOOLKIT_SCROLL_BARS TREE_SITTER WEBP XPM ZLIB

Important settings:
  value of $LANG: ENG
  locale-coding-system: cp1252

Major mode: Lean 4

Minor modes in effect:
  eglot--managed-mode: t
  flymake-mode: t
  tooltip-mode: t
  global-eldoc-mode: t
  eldoc-mode: t
  show-paren-mode: t
  mouse-wheel-mode: t
  tool-bar-mode: t
  menu-bar-mode: t
  file-name-shadow-mode: t
  global-font-lock-mode: t
  font-lock-mode: t
  blink-cursor-mode: t
  minibuffer-regexp-mode: t
  line-number-mode: t
  transient-mark-mode: t
  auto-composition-mode: t
  auto-encryption-mode: t
  auto-compression-mode: t

Features:
(shadow sort mail-extr emacsbug message mailcap yank-media puny rfc822
mml mml-sec epa derived epg rfc6068 epg-config gnus-util mm-decode
mm-bodies mm-encode mail-parse rfc2231 mailabbrev gmm-utils mailheader
sendmail rfc2047 rfc2045 ietf-drums mm-util mail-prsvr mail-utils
help-fns radix-tree cl-print files-x find-dired dired dired-loaddefs
grep time-date lean4-input quail comp comp-cstr cl-extra lean4-mode
lean4-fringe lean4-dev lean4-info magit-section format-spec
cursor-sensor compat lean4-syntax lean4-util lean4-settings f f-shortdoc
s lean4-eri eglot external-completion jsonrpc xref flymake thingatpt
project diff diff-mode easy-mmode ert pp ewoc debug backtrace filenotify
warnings icons compile text-property-search comint ansi-osc ring
url-util url-parse auth-source cl-seq eieio eieio-core cl-macs
password-cache url-vars imenu flycheck ansi-color json map byte-opt gv
bytecomp byte-compile find-func help-mode rx subr-x pcase dash
cl-loaddefs cl-lib cus-start cus-load rmc iso-transl tooltip cconv eldoc
paren electric uniquify ediff-hook vc-hooks lisp-float-type elisp-mode
mwheel dos-w32 ls-lisp disp-table term/w32-win w32-win w32-vars
term/common-win touch-screen tool-bar dnd fontset image regexp-opt
fringe tabulated-list replace newcomment text-mode lisp-mode prog-mode
register page tab-bar menu-bar rfn-eshadow isearch easymenu timer select
scroll-bar mouse jit-lock font-lock syntax font-core term/tty-colors
frame minibuffer nadvice seq simple cl-generic indonesian philippine
cham georgian utf-8-lang misc-lang vietnamese tibetan thai tai-viet lao
korean japanese eucjp-ms cp51932 hebrew greek romanian slovak czech
european ethiopic indian cyrillic chinese composite emoji-zwj charscript
charprop case-table epa-hook jka-cmpr-hook help abbrev obarray oclosure
cl-preloaded button loaddefs theme-loaddefs faces cus-face macroexp
files window text-properties overlay sha1 md5 base64 format env
code-pages mule custom widget keymap hashtable-print-readable backquote
threads w32notify w32 lcms2 multi-tty move-toolbar make-network-process
native-compile emacs)

Memory information:
((conses 16 230339 30888) (symbols 48 15071 0) (strings 32 50446 4052)
 (string-bytes 1 1546772) (vectors 16 36238)
 (vector-slots 8 716441 24950) (floats 8 77 40) (intervals 56 927 39)
 (buffers 992 18))