From 4b166acb98f9d7b9bab0cfc869b5cc57bfe8c149 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Wed, 8 Dec 2021 18:57:54 +0000 Subject: [PATCH 1/2] Update semantic highlighting code in line with the update IDE protocol 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) --- idris2-commands.el | 12 +++++++----- idris2-repl.el | 6 +++--- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/idris2-commands.el b/idris2-commands.el index 0d99e8a..05c23bb 100644 --- a/idris2-commands.el +++ b/idris2-commands.el @@ -227,8 +227,8 @@ A prefix argument forces loading but only up to the current line." (when (string= (file-name-nondirectory fn) (file-name-nondirectory (buffer-file-name))) (idris2-highlight-input-region (current-buffer) - start-line start-col - end-line end-col + (+ 1 start-line) (+ 1 start-col) + (+ 1 end-line ) (+ 1 end-col) props)))))) (_ (idris2-make-clean) (idris2-update-options-cache) @@ -364,14 +364,16 @@ compiler-annotated output. Does not return a line number." (defun idris2-jump-to-location (loc is-same-window) "jumps to specified location" - (pcase-let* ((`(,name ,file ,line ,col) loc) + (pcase-let* ((`(,name (:filename ,file) + (:start ,line ,col) + (:end ,_ ,_)) loc) (full-path file)) (xref-push-marker-stack) ;; this pushes a "tag" mark. haskell mode ;; also does this and it seems appropriate, allows the user to pop ;; the tag and go back to the previous point. (pop-tag-mark ;; default Ctl-t) (if full-path - (idris2-goto-source-location-full full-path (+ 1 line) col is-same-window) + (idris2-goto-source-location-full full-path (+ 1 line) (+ col 1) is-same-window) (user-error "Source not found for %s" file) ) ) @@ -386,7 +388,7 @@ compiler-annotated output. Does not return a line number." (let ((inhibit-read-only t)) (erase-buffer) (dolist (loc (reverse locs)) - (pcase-let* ((`(,name ,file ,line ,col) loc) + (pcase-let* ((`(,name (:filename ,file) ,_ ,_) loc) (fullpath file) ) (if (file-exists-p fullpath) diff --git a/idris2-repl.el b/idris2-repl.el index ee5a06d..597c3bf 100644 --- a/idris2-repl.el +++ b/idris2-repl.el @@ -354,9 +354,9 @@ Invokes `idris2-repl-mode-hook'." (input-col (save-excursion (goto-char start-pos) (current-column))) - (start-line-repl (+ input-line start-line -1)) - (start-col-repl (+ input-col start-col)) - (end-line-repl (+ input-line end-line -1)) + (start-line-repl (+ input-line start-line -1)) ;; Revisit these once we implement + (start-col-repl (+ input-col start-col)) ;; highlighting of repl inputs + (end-line-repl (+ input-line end-line -1)) ;; in case bounds need to be adjusted (end-col-repl (+ input-col end-col))) (idris2-highlight-input-region buffer start-line-repl start-col-repl From 89042604905aa83d23c0f2c7bbb1e618d567f2e3 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Wed, 8 Dec 2021 19:19:39 +0000 Subject: [PATCH 2/2] Fix off-by-1 error --- idris2-highlight-input.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/idris2-highlight-input.el b/idris2-highlight-input.el index 8834b4f..e866d73 100644 --- a/idris2-highlight-input.el +++ b/idris2-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) (idris2-highlight-column start-col))) (end-pos (+ (line-beginning-position end-line) - (idris2-highlight-column (+ 1 end-col)))) + (idris2-highlight-column end-col))) (highlight-overlay (make-overlay start-pos end-pos (get-buffer buffer)))) (overlay-put highlight-overlay 'idris2-source-highlight t)