From 8d69b7043233a9f26df2476e0c7539bc9f150295 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Wed, 8 Dec 2021 19:47:26 +0000 Subject: [PATCH 1/3] Update semantic highlighting code in line with the update IDE protocol Adds minor protocol version support See idris2 [PR#2171](https://github.com/idris-lang/Idris2/pull/2171)'s new spec for [`Bounds`](https://github.com/idris-lang/Idris2/blob/dd8914f627604461632bb530cb734014a47f505f/src/Libraries/Text/Bounded.idr#L9-L16) --- idris-commands.el | 20 ++++++++++++++++---- idris-highlight-input.el | 4 ++-- inferior-idris.el | 9 ++++++++- 3 files changed, 26 insertions(+), 7 deletions(-) diff --git a/idris-commands.el b/idris-commands.el index f7cb915f..00fb1525 100644 --- a/idris-commands.el +++ b/idris-commands.el @@ -229,15 +229,27 @@ A prefix argument forces loading but only up to the current line." for h in hs do (pcase h (`(((:filename ,fn) - (:start ,start-line ,start-col) - (:end ,end-line ,end-col)) + (:start ,start-line-raw ,start-col-raw) + (:end ,end-line-raw ,end-col-raw)) ,props) (when (string= (file-name-nondirectory fn) (file-name-nondirectory (buffer-file-name))) - (idris-highlight-input-region (current-buffer) + (let ((start-line (if (>=-protocol-version 2 1) + (+ 1 start-line-raw) + start-line-raw)) + (start-col (if (>=-protocol-version 2 1) + (+ 1 start-col-raw) + start-col-raw)) + (end-line (if (>=-protocol-version 2 1) + (+ 1 end-line-raw) + end-line-raw )) + (end-col (if (>= idris-protocol-version 2 1) + (+ 1 end-col-raw) + end-col-raw ))) + (idris-highlight-input-region (current-buffer) start-line start-col end-line end-col - props)))))) + props))))))) (_ (idris-make-clean) (idris-update-options-cache) diff --git a/idris-highlight-input.el b/idris-highlight-input.el index 56f46a62..396ff202 100644 --- a/idris-highlight-input.el +++ b/idris-highlight-input.el @@ -60,14 +60,14 @@ See Info node `(elisp)Overlay Properties' to understand how ARGS are used." (widen) (if (or (> end-line start-line) (and (= end-line start-line) - (>= end-col start-col))) + (> end-col start-col))) (with-current-buffer buffer (save-excursion (goto-char (point-min)) (let* ((start-pos (+ (line-beginning-position start-line) (idris-highlight-column start-col))) (end-pos (+ (line-beginning-position end-line) - (idris-highlight-column (+ 1 end-col)))) + (idris-highlight-column end-col))) (highlight-overlay (make-overlay start-pos end-pos (get-buffer buffer)))) (overlay-put highlight-overlay 'idris-source-highlight t) diff --git a/inferior-idris.el b/inferior-idris.el index ac818c2e..4e70d57a 100644 --- a/inferior-idris.el +++ b/inferior-idris.el @@ -67,11 +67,18 @@ "The Idris connection.") (defvar idris-protocol-version 0 "The protocol version") +(defvar idris-protocol-version-minor 0 "The protocol minor version") + +(defun >=-protocol-version (major minor) + (or (> idris-protocol-version major) + (and (>= idris-protocol-version major) + (>= idris-protocol-version-minor minor)))) (defun idris-version-hook-function (event) (pcase event - (`(:protocol-version ,version ,_target) + (`(:protocol-version ,version ,minor) (setf idris-protocol-version version) + (setf idris-protocol-version-minor minor) (remove-hook 'idris-event-hooks 'idris-version-hook-function) t))) From e3d1266db6765bf2e1a24fb4e86090a8bbc12a72 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Thu, 9 Dec 2021 15:05:49 +0000 Subject: [PATCH 2/3] Fix more 'bounds' to spec in newer IDE protocols --- idris-warnings.el | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/idris-warnings.el b/idris-warnings.el index bec2ad1a..927d6a9c 100644 --- a/idris-warnings.el +++ b/idris-warnings.el @@ -81,10 +81,18 @@ WARNING is of form (filename (startline startcolumn) (endline endcolumn) message As of 20140807 (Idris 0.9.14.1-git:abee538) (endline endcolumn) is mostly the same as (startline startcolumn) " (cl-destructuring-bind (filename sl1 sl2 message spans) warning - (let ((startline (nth 0 sl1)) - (startcol (1- (nth 1 sl1))) - (endline (nth 0 sl2)) - (endcol (1- (nth 1 sl2)))) + (let ((startline (if (>=-protocol-version 2 1) + (1+ (nth 0 sl1)) + (nth 0 sl1))) + (startcol (if (>=-protocol-version 2 1) + (nth 1 sl1) + (1- (nth 1 sl1)))) + (endline (if (>=-protocol-version 2 1) + (1+ (nth 0 sl2)) + (nth 0 sl2))) + (endcol (if (>=-protocol-version 2 1) + (nth 1 sl2) + (1- (nth 1 sl2))))) (push (list filename startline startcol message spans) idris-raw-warnings) (let* ((fullpath (concat (file-name-as-directory idris-process-current-working-directory) filename)) From fce35c43492493c979d56a9d4f585c4173f4e80b Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 20 Dec 2021 13:00:15 +0000 Subject: [PATCH 3/3] Move idris-protocol-version vars and access function to common-utils to avoid circular module dependency --- idris-common-utils.el | 8 ++++++++ inferior-idris.el | 8 -------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/idris-common-utils.el b/idris-common-utils.el index d08b451a..be9b8c43 100644 --- a/idris-common-utils.el +++ b/idris-common-utils.el @@ -402,4 +402,12 @@ relative to SRC-DIR" (when (file-exists-p lidr) (make-link lidr)))))) +(defvar idris-protocol-version 0 "The protocol version") +(defvar idris-protocol-version-minor 0 "The protocol minor version") + +(defun >=-protocol-version (major minor) + (or (> idris-protocol-version major) + (and (>= idris-protocol-version major) + (>= idris-protocol-version-minor minor)))) + (provide 'idris-common-utils) diff --git a/inferior-idris.el b/inferior-idris.el index 4e70d57a..7f73923f 100644 --- a/inferior-idris.el +++ b/inferior-idris.el @@ -66,14 +66,6 @@ (defvar idris-connection nil "The Idris connection.") -(defvar idris-protocol-version 0 "The protocol version") -(defvar idris-protocol-version-minor 0 "The protocol minor version") - -(defun >=-protocol-version (major minor) - (or (> idris-protocol-version major) - (and (>= idris-protocol-version major) - (>= idris-protocol-version-minor minor)))) - (defun idris-version-hook-function (event) (pcase event (`(:protocol-version ,version ,minor)