[nongnu] elpa/idris-mode c9b2a4bee6 10/13: Add Xref backend for Idris

[ELPA Syncer]

branch: elpa/idris-mode
commit c9b2a4bee6eeffe474304a0c728ebdd910230b5b
Author: Marek L <nospam.keram@gmail.com>
Commit: Marek L <nospam.keram@gmail.com>

    Add Xref backend for Idris
    
    Why:
    This provides "jump to definition" funcionality
    for "*.idr" files and Idris repl.
---
 Makefile           |   1 +
 idris-mode.el      |   6 +-
 idris-repl.el      |   4 +-
 idris-tests.el     |   5 +-
 idris-xref-test.el | 328 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 idris-xref.el      | 147 ++++++++++++++++++++++++
 6 files changed, 486 insertions(+), 5 deletions(-)

diff --git a/Makefile b/Makefile
index e7daf04452..c80e51c4bb 100644
--- a/Makefile
+++ b/Makefile
@@ -37,6 +37,7 @@ OBJS =        idris-commands.elc              \
        idris-syntax.elc                \
        idris-warnings.elc              \
        idris-warnings-tree.elc         \
+       idris-xref.elc \
        inferior-idris.elc
 
 .el.elc:
diff --git a/idris-mode.el b/idris-mode.el
index 7d95895f94..4d408897b3 100644
--- a/idris-mode.el
+++ b/idris-mode.el
@@ -29,7 +29,7 @@
 (require 'idris-warnings)
 (require 'idris-common-utils)
 (require 'idris-ipkg-mode)
-
+(require 'idris-xref)
 
 (defun idris-mode-context-menu-items (plist)
   "Compute menu items from PLIST that are specific to editing text in 
`idris-mode'."
@@ -162,7 +162,9 @@ Invokes `idris-mode-hook'."
   (when (idris-lidr-p)
     (run-hooks 'idris-mode-lidr-hook))
   (set (make-local-variable 'prop-menu-item-functions)
-       '(idris-context-menu-items idris-mode-context-menu-items)))
+       '(idris-context-menu-items idris-mode-context-menu-items))
+
+  (add-hook 'xref-backend-functions #'idris-xref-backend nil 'local))
 
 ;; Automatically use idris-mode for .idr and .lidr files.
 ;;;###autoload
diff --git a/idris-repl.el b/idris-repl.el
index 3a0d457800..7862a3ddd4 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -34,6 +34,7 @@
 (require 'idris-common-utils)
 (require 'idris-prover)
 (require 'idris-highlight-input)
+(require 'idris-xref)
 
 (eval-when-compile (require 'cl-lib))
 
@@ -229,7 +230,8 @@ Invokes `idris-repl-mode-hook'."
   (set (make-local-variable 'completion-at-point-functions) 
'(idris-repl-complete))
   (setq mode-name `("Idris-REPL" (:eval (if idris-rex-continuations "!" ""))))
   (set (make-local-variable 'prop-menu-item-functions)
-       '(idris-context-menu-items)))
+       '(idris-context-menu-items))
+  (add-hook 'xref-backend-functions #'idris-xref-backend nil 'local))
 
 (defun idris-repl-remove-event-hook-function ()
   (setq idris-prompt-string "Idris")
diff --git a/idris-tests.el b/idris-tests.el
index 2c3e9f5ac6..5f3476ab04 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -189,7 +189,7 @@ remain."
   (with-current-buffer (get-buffer idris-info-buffer-name)
     (goto-char (point-min))
     (should (re-search-forward "Zero" nil t)))
- (idris-quit))
+  (idris-quit))
 
 (ert-deftest idris-test-ipkg-packages-with-underscores-and-dashes ()
   "Test that loading an ipkg file can have dependencies on packages with _ or 
- in the name."
@@ -322,7 +322,7 @@ myReverse xs = revAcc [] xs where
                        "Some warning message"))
       ;; Cleanup
       (kill-buffer))))
-       
+
 (ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
   "Test idris-backard-toplevel navigation command."
   (idris-test-with-temp-buffer
@@ -576,5 +576,6 @@ getData2 st failcount
    (should (looking-back "Store LoggedOut)]" (line-beginning-position)))
    ))
 
+(load "idris-xref-test.el")
 (provide 'idris-tests)
 ;;; idris-tests.el ends here
diff --git a/idris-xref-test.el b/idris-xref-test.el
new file mode 100644
index 0000000000..57d62cb63e
--- /dev/null
+++ b/idris-xref-test.el
@@ -0,0 +1,328 @@
+;;; idris-xref-test.el --- Tests for Idris Xref backend  -*- lexical-binding: 
t -*-
+;; Copyright (C) 2022  Marek L.
+
+;; Author: Marek L <nospam.keram@gmail.com>
+;; Keywords: languages, Idris, Xref, Ert
+
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+;;; Code:
+
+(require 'ert)
+(require 'idris-xref)
+
+(ert-deftest idris-xref-backend-definitions--error-when-no-connection ()
+  "Test that the file is loaded before making search for definition."
+  (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
+        (inhibit-read-only t))
+    (with-current-buffer "*Messages*" (erase-buffer))
+    (with-current-buffer buffer
+      (goto-char (point-min))
+      (search-forward ": Test")
+      (condition-case err
+          (funcall-interactively 'xref-find-definitions "Test")
+        (error (message "Error: %s" (error-message-string err)))
+        (user-error (message "User Error: %s" (error-message-string err)))))
+
+    (with-current-buffer "*Messages*"
+      (should
+       (string-match-p "Buffer AddClause.idr has no process"
+                       (buffer-substring-no-properties (point-min) 
(point-max)))))
+
+    ;; Cleanup
+    (kill-buffer buffer)))
+
+(ert-deftest idris-xref-backend-definitions--not-supported-on-Idris-1 ()
+  "Test that user error raised when invoking `xref-find-definitions' used on 
Idris1."
+  (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
+        (err-msg "did not understand (synchronous Idris evaluation failed)")
+        (inhibit-read-only t))
+    (with-current-buffer "*Messages*" (erase-buffer))
+    (cl-flet ((idris-load-file-sync-stub () nil)
+              (idris-eval-stub (&optional &rest _args)
+                               (user-error err-msg)))
+      (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+      (advice-add 'idris-eval :override #'idris-eval-stub)
+
+      (unwind-protect
+          (with-current-buffer buffer
+            (goto-char (point-min))
+            (search-forward ": Test")
+
+            (condition-case err
+                (funcall-interactively 'xref-find-definitions "Test")
+              (error (message "%s" (error-message-string err)))))
+
+        (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+        (advice-remove 'idris-eval #'idris-eval-stub)))
+
+    (with-current-buffer "*Messages*"
+      (should
+       (string-match-p err-msg (buffer-substring-no-properties (point-min) 
(point-max)))))
+
+    ;; Cleanup
+    (kill-buffer buffer)))
+
+(ert-deftest idris-xref-backend-definitions--no-results ()
+  "Test that an user error message is displayed when no definition found."
+  ;; Arrange
+  (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
+        (idris-protocol-version 3)
+        (inhibit-read-only t))
+    (with-current-buffer "*Messages*" (erase-buffer))
+    (cl-flet ((idris-load-file-sync-stub () nil)
+              (idris-eval-stub (&optional &rest _args) '()))
+      (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+      (advice-add 'idris-eval :override #'idris-eval-stub)
+
+      (unwind-protect
+          (with-current-buffer buffer
+            (goto-char (point-min))
+            (search-forward ": Test")
+            ;; (with-demoted-errors "Error: %s"
+            ;;   ;; Act
+            ;;   (funcall-interactively 'xref-find-definitions "Test"))
+            (condition-case err
+                (funcall-interactively 'xref-find-definitions "Test")
+              (user-error (message "%s" (error-message-string err)))))
+
+        (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+        (advice-remove 'idris-eval #'idris-eval-stub)))
+
+    (with-current-buffer "*Messages*"
+      ;; Assert
+      (should
+       (string-match-p "No definitions found for: Test"
+                       (buffer-substring-no-properties (point-min) 
(point-max)))))
+    ;; Cleanup
+    (kill-buffer buffer)))
+
+(ert-deftest idris-xref-backend-definitions--one-existing-file-result ()
+  "Test that point jumps to location in file from result."
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (idris-protocol-version 3)
+         (eval-result `((("AddClause.Test"
+                          (:filename ,(buffer-file-name buffer))
+                          (:start 2 0)
+                          (:end 2 17)))))
+         (inhibit-read-only t))
+    (with-current-buffer "*Messages*" (erase-buffer))
+    (cl-flet ((idris-load-file-sync-stub () nil)
+              (idris-eval-stub (&optional &rest _args) eval-result))
+      (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+      (advice-add 'idris-eval :override #'idris-eval-stub)
+
+      (unwind-protect
+          (with-current-buffer buffer
+            (goto-char (point-min))
+            (search-forward ": Test")
+            (should (eq 6 (line-number-at-pos (point))))
+
+            (condition-case err
+                (funcall-interactively 'xref-find-definitions "Test")
+              (user-error (message "%s" (error-message-string err))))
+
+            (should (eq 3 (line-number-at-pos (point)))))
+
+        (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+        (advice-remove 'idris-eval #'idris-eval-stub)))
+
+    ;; Cleanup
+    (kill-buffer buffer)))
+
+(ert-deftest idris-xref-backend-definitions--one-no-real-file-result ()
+  "Test that the term and filename as message is displayed."
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (idris-protocol-version 3)
+         (eval-result `((("prim__lte_Bits64"
+                          (:filename "(Interactive)")
+                          (:start 0 0)
+                          (:end 0 0)))))
+         (inhibit-read-only t))
+    (with-current-buffer "*Messages*" (erase-buffer))
+    (cl-flet ((idris-load-file-sync-stub () nil)
+              (idris-eval-stub (&optional &rest _args) eval-result))
+      (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+      (advice-add 'idris-eval :override #'idris-eval-stub)
+
+      (unwind-protect
+          (with-current-buffer buffer
+            (goto-char (point-min))
+            (search-forward ": Test")
+            ;; (with-demoted-errors "Error: %s"
+            ;;   ;; Act
+            ;;   (funcall-interactively 'xref-find-definitions "Test"))
+            (condition-case err
+                (funcall-interactively 'xref-find-definitions "Test")
+              (user-error (message "%s" (error-message-string err)))))
+
+        (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+        (advice-remove 'idris-eval #'idris-eval-stub)))
+
+    (with-current-buffer "*Messages*"
+      ;; Assert
+      (should
+       (string-match-p "prim__lte_Bits64 : (Interactive)"
+                       (buffer-substring-no-properties (point-min) 
(point-max)))))
+    ;; Cleanup
+    (kill-buffer buffer)))
+
+(ert-deftest idris-xref-backend-definitions--multiple-results ()
+  "Test that results are listed in *xref* buffer."
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (idris-protocol-version 3)
+         (eval-result `((("prim__lte_Bits64"
+                          (:filename "(Interactive)")
+                          (:start 0 0)
+                          (:end 0 0))
+                         ("Prelude.Num.(-)"
+                          (:filename "(File-Not-Found)")
+                          (:start 30 2)
+                          (:end 30 5))
+                         ("AddClause.(-)"
+                          (:filename "AddClause.idr")
+                          (:start 10 0)
+                          (:end 10 9))))))
+    (cl-flet ((idris-load-file-sync-stub () nil)
+              (idris-eval-stub (&optional &rest _args) eval-result))
+      (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+      (advice-add 'idris-eval :override #'idris-eval-stub)
+
+      (unwind-protect
+          (with-current-buffer buffer
+            (goto-char (point-min))
+            (search-forward ": Test")
+            ;; (with-demoted-errors "Error: %s"
+            ;;   ;; Act
+            ;;   (funcall-interactively 'xref-find-definitions "Test"))
+            (condition-case err
+                (funcall-interactively 'xref-find-definitions "Test")
+              (user-error (message "%s" (error-message-string err)))))
+
+        (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+        (advice-remove 'idris-eval #'idris-eval-stub)))
+
+    (with-current-buffer "*xref*"
+      ;; Assert
+      (let ((str (buffer-substring-no-properties (point-min) (point-max))))
+        (should (string-match-p "11: AddClause.(-)" str))
+        (should (string-match-p "AddClause.idr" str))
+        (should (string-match-p "Prelude.Num.(-)" str))
+        (should (string-match-p "prim__lte_Bits64" str)))
+      (kill-buffer))
+
+    ;; Cleanup
+    (kill-buffer buffer)))
+
+(ert-deftest idris-xref-normalise ()
+  "Test normalisation of results from Idris compiler.
+The updated candidate should have absolute path to file when possible
+and coordinates indexed as expected by Emacs."
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (candidate `("AddClause.Test"
+                      (:filename ,(buffer-file-name buffer))
+                      (:start 2 0)
+                      (:end 2 17)))
+         (result (idris-xref-normalise candidate)))
+
+    (pcase-let ((`(,_term (:filename ,fn)
+                          (:start ,start-line ,start-col)
+                          (:end ,_end-line ,_end-col))
+                 result))
+      (should (string= fn (buffer-file-name buffer)))
+      (should (eq start-line 3))
+      (should (eq start-col 1))))
+
+  ;; Test that the filepath is reconstructed from term
+  ;; and Idris process current working directory
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (candidate `("AddClause.Test"
+                      (:filename "(File-Not-Found)")
+                      (:start 2 0)
+                      (:end 2 17)))
+         (idris-process-current-working-directory (file-name-directory 
(buffer-file-name buffer)))
+         (result (idris-xref-normalise candidate)))
+
+    (pcase-let ((`(,_term (:filename ,fn)
+                          (:start ,start-line ,start-col)
+                          (:end ,_end-line ,_end-col))
+                 result))
+      (should (string= fn (buffer-file-name buffer)))
+      (should (eq start-line 3))
+      (should (eq start-col 1))))
+
+  ;; Test that the original filename returned if no success to
+  ;; reconstruct real absolute file path
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (candidate `("AddClause.Test"
+                      (:filename "(File-Not-Found)")
+                      (:start 2 0)
+                      (:end 2 17)))
+         (idris-process-current-working-directory nil)
+         (result (idris-xref-normalise candidate)))
+
+    (pcase-let ((`(,_term (:filename ,fn)
+                          (:start ,start-line ,start-col)
+                          (:end ,_end-line ,_end-col))
+                 result))
+      (should (string= fn "(File-Not-Found)"))
+      (should (eq start-line 3))
+      (should (eq start-col 1))))
+
+  ;; Test that the filepath is reconstructed from term
+  ;; and (idris-xref-idris-source-directories)
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (candidate `("AddClause.Test"
+                      (:filename "(File-Not-Found)")
+                      (:start 2 0)
+                      (:end 2 17)))
+         (idris-process-current-working-directory nil))
+    (cl-flet ((idris-xref-idris-source-directories-stub
+               ()
+               (cons (file-name-directory (buffer-file-name buffer)) '())))
+      (advice-add 'idris-xref-idris-source-directories
+                  :override #'idris-xref-idris-source-directories-stub)
+
+      (let ((result (idris-xref-normalise candidate)))
+        (pcase-let ((`(,_term (:filename ,fn)
+                              (:start ,start-line ,start-col)
+                              (:end ,_end-line ,_end-col))
+                     result))
+
+          (should (string= fn (buffer-file-name buffer)))
+          (should (eq start-line 3))
+          (should (eq start-col 1))))
+      (advice-remove 'idris-xref-idris-source-directories
+                     #'idris-xref-idris-source-directories-stub)))
+
+  ;; Test that the filepath is reconstructed from term
+  ;; and path from idris-xref-idris-source-locations
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (candidate `("AddClause.Test"
+                      (:filename "(File-Not-Found)")
+                      (:start 2 0)
+                      (:end 2 17)))
+         (idris-xref-idris-source-locations (cons (file-name-directory 
(buffer-file-name buffer)) '()))
+         (result (idris-xref-normalise candidate)))
+
+    (pcase-let ((`(,_term (:filename ,fn)
+                          (:start ,start-line ,start-col)
+                          (:end ,_end-line ,_end-col))
+                 result))
+      (should (string= fn (buffer-file-name buffer)))
+      (should (eq start-line 3))
+      (should (eq start-col 1)))))
+
+(provide 'idris-xref-test)
+;;; idris-xref-test.el ends here
diff --git a/idris-xref.el b/idris-xref.el
new file mode 100644
index 0000000000..bbc6cb88da
--- /dev/null
+++ b/idris-xref.el
@@ -0,0 +1,147 @@
+;;; idris-xref.el --- Xref backend for Idris  -*- lexical-binding: t -*-
+;; Copyright (C) 2022  Marek L.
+
+;; Author: Marek L <nospam.keram@gmail.com>
+;; Keywords: languages, Idris, Xref
+
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+;;; Commentary:
+;;
+
+;;; Code:
+
+(require 'xref)
+(require 'inferior-idris)
+(require 'idris-common-utils)
+
+;; TODO: Define as idris-file-extension
+(defconst idris-xref-idris-file-extension "idr")
+
+(defgroup idris-xref nil "Idris Xref Backend." :prefix 'idris :group 'idris)
+
+(defcustom idris-xref-idris-source-location ""
+  "Path to local Idris language codebase repository."
+  :type 'directory
+  :group 'idris-xref)
+
+(defcustom idris-xref-idris-source-locations '()
+  "List of additional directories to perform lookup for a term.
+To support jump to definition for Idris build-in types
+set `idris-xref-idris-source-location' instead."
+  :type '(repeat directory)
+  :group 'idris-xref)
+
+;; TODO: Memoize
+(defun idris-xref-idris-source-directories ()
+  "Return list of directories from Idris repository to do lookup for a term."
+  (when (and idris-xref-idris-source-location (file-directory-p 
idris-xref-idris-source-location))
+    (let ((src-dir (expand-file-name "src" idris-xref-idris-source-location))
+          (libs-dir (expand-file-name "libs" 
idris-xref-idris-source-location)))
+      (when (and (file-directory-p src-dir) (file-directory-p libs-dir))
+        (cons src-dir
+              (seq-filter #'file-directory-p
+                          (mapcar (lambda (dir) (expand-file-name dir 
libs-dir))
+                                  (seq-remove (lambda (dir) (string-match-p 
"\\." dir))
+                                              (directory-files 
libs-dir)))))))))
+
+(defun idris-xref-backend ()
+  "An `xref-backend-functions' implementation for `idris-mode'."
+  'idris)
+
+(cl-defmethod xref-backend-identifier-at-point ((_backend (eql idris)))
+  "Alias for `idris-name-at-point'."
+  (idris-name-at-point))
+
+(cl-defmethod xref-backend-definitions ((_backend (eql idris)) symbol)
+  "Return a list of Xref objects candidates matching SYMBOL."
+
+  (mapcar #'idris-xref-make-xref
+          (mapcar #'idris-xref-normalise (idris-xref-find-definitions 
symbol))))
+
+(cl-defmethod xref-backend-apropos ((_backend (eql idris)))
+  "Not yet supported."
+  nil)
+
+(cl-defmethod xref-backend-identifier-completion-table ((_backend (eql idris)))
+  "Not yet supported."
+  nil)
+
+(defun idris-xref-find-definitions (symbol)
+  "Return a list of Idris candidate locations matching SYMBOL."
+  (car (idris-eval `(:name-at ,symbol))))
+
+(defun idris-xref-normalise (candidate)
+  "Return normalised CANDIDATE.
+
+It will try add filename absolute path if not present and
+update coordinates to be indexed from 1 as expected by Emacs."
+  (pcase-let ((`(,term (:filename ,fn)
+                       (:start ,start-line ,start-col)
+                       (:end ,end-line ,end-col))
+               candidate))
+    (let ((new-fn (idris-xref-filepath term fn)))
+      `(,term (:filename ,new-fn)
+              (:start ,(1+ start-line) ,(1+ start-col))
+              (:end ,(1+ end-line) ,(1+ end-col))))))
+
+(defun idris-xref-make-xref (location)
+  "Return a new Xref object from LOCATION."
+  (pcase-let ((`(,term (:filename ,fn)
+                       (:start ,start-line ,start-col)
+                       (:end ,_end-line ,_end-col))
+               location))
+    (xref-make term
+               (if (file-exists-p fn)
+                   (xref-make-file-location fn start-line start-col)
+                 (xref-make-bogus-location (format "%s : %s" term fn))))))
+
+(defun idris-xref-filepath (term file)
+  "Return filepath for TERM.
+If FILE is path to existing file returns the FILE.
+Otherwise try find the corresponding FILE for TERM in 
`idris-xref-directories'."
+  (if (file-exists-p file)
+      file
+    (let ((file-paths (idris-xref-abs-filepaths term 
(idris-xref-directories))))
+      (if (null file-paths)
+          file
+        ;; TODO: Instead of getting the first filepath build list of candidates
+        (car file-paths)))))
+
+(defun idris-xref-directories ()
+  "List of directories to perform lookup for file containing a term.
+The list consist of `idris-process-current-working-directory',
+`idris-xref-idris-source-directories' and `idris-xref-idris-source-locations'."
+  (append
+    (and idris-process-current-working-directory (list 
idris-process-current-working-directory))
+    (idris-xref-idris-source-directories)
+    (seq-filter #'file-directory-p idris-xref-idris-source-locations)))
+
+(defun idris-xref-relative-filepath-from-term (term)
+  "Return relative Idris file path created from TERM."
+  (let* ((term-parts (reverse (butlast (split-string term "\\."))))
+         (file-base (pop term-parts))
+         (file-name (concat file-base "." idris-xref-idris-file-extension)))
+    (apply 'idris-file-name-concat (reverse (cons file-name term-parts)))))
+
+(defun idris-xref-abs-filepaths (term locations)
+  "Return absolute filepaths build from TERM and LOCATIONS."
+  (let ((rel-path (idris-xref-relative-filepath-from-term term)))
+    ;; TODO: Check also the content of file for presence of the term
+    (seq-filter #'file-exists-p
+                (mapcar (lambda (loc) (expand-file-name rel-path loc))
+                        locations))))
+
+(provide 'idris-xref)
+;;; idris-xref.el ends here