From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Richard Copley Newsgroups: gmane.emacs.bugs Subject: bug#66552: 30.0.50; Eglot feature request: handle quirky code actions Date: Sun, 15 Oct 2023 03:24:45 +0100 Message-ID: Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="4509"; mail-complaints-to="usenet@ciao.gmane.io" To: 66552@debbugs.gnu.org Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Sun Oct 15 04:25:57 2023 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1qrqpI-00011g-84 for geb-bug-gnu-emacs@m.gmane-mx.org; Sun, 15 Oct 2023 04:25:56 +0200 Original-Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1qrqp1-00014x-HD; Sat, 14 Oct 2023 22:25:39 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qrqp0-00014p-P7 for bug-gnu-emacs@gnu.org; Sat, 14 Oct 2023 22:25:38 -0400 Original-Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qrqp0-0008MR-H2 for bug-gnu-emacs@gnu.org; Sat, 14 Oct 2023 22:25:38 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1qrqpO-0006vE-2v for bug-gnu-emacs@gnu.org; Sat, 14 Oct 2023 22:26:02 -0400 X-Loop: help-debbugs@gnu.org Resent-From: Richard Copley Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Sun, 15 Oct 2023 02:26:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 66552 X-GNU-PR-Package: emacs X-Debbugs-Original-To: bug-gnu-emacs@gnu.org Original-Received: via spool by submit@debbugs.gnu.org id=B.169733675926597 (code B ref -1); Sun, 15 Oct 2023 02:26:01 +0000 Original-Received: (at submit) by debbugs.gnu.org; 15 Oct 2023 02:25:59 +0000 Original-Received: from localhost ([127.0.0.1]:51011 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qrqpK-0006uv-Mg for submit@debbugs.gnu.org; Sat, 14 Oct 2023 22:25:59 -0400 Original-Received: from lists.gnu.org ([2001:470:142::17]:58612) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qrqpE-0006ue-Ts for submit@debbugs.gnu.org; Sat, 14 Oct 2023 22:25:57 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qrqoj-000145-AF for bug-gnu-emacs@gnu.org; Sat, 14 Oct 2023 22:25:21 -0400 Original-Received: from mail-qt1-x82e.google.com ([2607:f8b0:4864:20::82e]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qrqod-0008Lg-Rw for bug-gnu-emacs@gnu.org; Sat, 14 Oct 2023 22:25:21 -0400 Original-Received: by mail-qt1-x82e.google.com with SMTP id d75a77b69052e-417f872fb94so23875451cf.0 for ; Sat, 14 Oct 2023 19:25:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1697336712; x=1697941512; darn=gnu.org; h=to:subject:message-id:date:from:mime-version:from:to:cc:subject :date:message-id:reply-to; bh=9J5lddnFr1cRjusPg7ZJMUQqIpOO+OaGde57A/D9LsA=; b=j+sSrhZLpfMd76YZtGOR942gBTD/cw2w9eoP4ONNkjfCVS7urWInFwDPzYqmMPgcT2 6OyJoV8FdGzm1kCn8bUjARROuyLIDxZZe8n8mj14DT6jBDKSXmDhlfVeyeo8ALH0vX5x 0dTGmsvAD0qcMH15dij+sS9/EWlQo4U9c0DG0wyoyGOAgPLfSNfhqM8GHr8L8kCPYWvl Um5J4vQz+F2h1nXSvrDKUMJCUy0HQysorCaembEMyxzjf6s/jqiNKkrZbUiGf5f814Lo tkbESHhLREXKpGbYODDPN1uV6TQu0tczRAjQ/IeklfmA70dFHVresBPeLxvVOutfZqPA QQ/A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1697336712; x=1697941512; h=to:subject:message-id:date:from:mime-version:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=9J5lddnFr1cRjusPg7ZJMUQqIpOO+OaGde57A/D9LsA=; b=LJWr5BVZyRuZE5jC4VvhfWG8r1PDMJZG2VBj54BNELa7ITuLuz3uPmviyoXQxqX6uC 2VoAeljbnCrFNXZjopZtmIhB1SP/ra0vuvU02wpFNTxjTHTcguz4NGLHzvpxfACDmXh6 VINqy9bnsK8RRiQYuNdY0kfTHhF9AE7yH+uAQSA8lcG7zFrmRJVRN1Y43PHScI/YoFFq HeWtjONOoBQ5A1tkgUvRZW4Uuthn/J902el+GNRKBHHXXjncdfcTEwZptBq9K0Igkjag 86l0UH77SZ8fjeAtenRHhohHohgf5revOl/Q1IUu/BJgFLhJyJBFJMUY04rGQ4FLGROR MqxA== X-Gm-Message-State: AOJu0YxpnGYszfOMsyNSUmp5/y/gokTZ/sTu0MhXP4x5pvfgdOvke8Ew dvfpcdySYii7j4j7fRmpjFpWCeAvh75jV1rKKPZD7123yXo= X-Google-Smtp-Source: AGHT+IE1yX4EO6BsBIjilBISwP7ae0Pnec/PbwM1x1TaUvh+varZtvosFopz3raahFJWo0aVV7JePQrjrxXS8DAQCGw= X-Received: by 2002:ac8:5f8c:0:b0:417:9431:c61b with SMTP id j12-20020ac85f8c000000b004179431c61bmr37771080qta.18.1697336712308; Sat, 14 Oct 2023 19:25:12 -0700 (PDT) Received-SPF: pass client-ip=2607:f8b0:4864:20::82e; envelope-from=rcopley@gmail.com; helo=mail-qt1-x82e.google.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, T_SPF_TEMPERROR=0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Xref: news.gmane.io gmane.emacs.bugs:272479 Archived-At: 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))