Update semantic highlighting code in line with the update IDE protocol (

#11) * Update semantic highlighting code in line with the update IDE protocol See idris2 [PR#2171](idris-lang/Idris2#2171 new spec for [`Bounds`](https://github.com/idris-lang/Idris2/blob/dd8914f627604461632bb530cb734014a47f505f/src/Libraries/Text/Bounded.idr#L9-L16) * Fix off-by-1 error Co-authored-by: Ohad Kammar <[email protected]>
idris-community · Dec 19, 2021 · 0ea481d · 0ea481d
1 parent b035de5
commit 0ea481d
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 10 deletions.
diff --git 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-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)

diff --git 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