From 269444381230e94a792e7bf8afcadcf52f89342a Mon Sep 17 00:00:00 2001
From: Marek L <nospam.keram@gmail.com>
Date: Tue, 9 Jul 2024 00:11:34 +0100
Subject: [PATCH] Improve idris-filename-to-load to return a pair of

"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
https://github.com/idris-lang/Idris2/issues/3310
https://github.com/idris-hackers/idris-mode/pull/627
---
 idris-commands.el           | 16 +++++++--------
 test/idris-commands-test.el | 40 +++++++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 8 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index 95975e1..9302948 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -168,14 +168,14 @@
 (defun idris-filename-to-load ()
   "Compute the working directory and filename to load in Idris.
 Returning these as a cons."
-  (let* ((fn (buffer-file-name))
-         (ipkg-srcdir (idris-ipkg-find-src-dir))
-         (srcdir (or ipkg-srcdir (file-name-directory fn))))
-    (when (and  ;; check that srcdir is prefix of filename - then load relative
-           (> (length fn) (length srcdir))
-           (string= (substring fn 0 (length srcdir)) srcdir))
-      (setq fn (file-relative-name fn srcdir)))
-    (cons srcdir fn)))
+  (let* ((ipkg-file (car-safe (idris-find-file-upwards "ipkg")))
+         (file-name (buffer-file-name))
+         (work-dir (directory-file-name (file-name-parent-directory (or ipkg-file file-name))))
+         (source-dir (or (idris-ipkg-find-src-dir) work-dir)))
+    ;; TODO: Update once https://github.com/idris-lang/Idris2/issues/3310 is resolved
+    (if (> idris-protocol-version 1)
+        (cons work-dir (file-relative-name file-name work-dir))
+      (cons source-dir (file-relative-name file-name source-dir)))))
 
 (defun idris-load-file (&optional set-line)
   "Pass the current buffer's file to the inferior Idris process.
diff --git a/test/idris-commands-test.el b/test/idris-commands-test.el
index 4d1f95e..7c38bcc 100644
--- a/test/idris-commands-test.el
+++ b/test/idris-commands-test.el
@@ -313,6 +313,46 @@ myReverse xs = revAcc [] xs where
       (delete-directory mock-directory-name t)
       (idris-quit))))
 
+(ert-deftest idris-test-idris-filename-to-load ()
+  "Test that `idris-filename-to-load' returns expected data structure."
+  (cl-flet ((idris-ipkg-find-src-dir-stub () src-dir)
+            (idris-find-file-upwards-stub (_ex) ipkg-files)
+            (buffer-file-name-stub () "/some/path/to/idris-project/src/Component/Foo.idr"))
+    (advice-add 'idris-ipkg-find-src-dir :override #'idris-ipkg-find-src-dir-stub)
+    (advice-add 'idris-find-file-upwards :override #'idris-find-file-upwards-stub)
+    (advice-add 'buffer-file-name :override #'buffer-file-name-stub)
+    (let* ((default-directory "/some/path/to/idris-project/src/Component")
+           ipkg-files
+           src-dir)
+      (unwind-protect
+          (progn
+            (let ((result (idris-filename-to-load)))
+              (should (equal default-directory (car result)))
+              (should (equal "Foo.idr" (cdr result))))
+
+            ;; When ipkg sourcedir value is set
+            ;; Then return combination of source directory
+            ;; and relative path of the file to the source directory
+            (let* ((src-dir "/some/path/to/idris-project/src")
+                   (result (idris-filename-to-load)))
+              (should (equal src-dir (car result)))
+              (should (equal "Component/Foo.idr" (cdr result))))
+
+            ;; When ipkg sourcedir value is set
+            ;; and idris-protocol-version is greater than 1
+            ;; Then return combination of work directory
+            ;; (Directory containing the first found ipkg file)
+            ;; and relative path of the file to the work directory
+            (let* ((ipkg-files '("/some/path/to/idris-project/baz.ipkg"))
+                   (idris-protocol-version 2)
+                   (result (idris-filename-to-load)))
+              (should (equal "/some/path/to/idris-project" (car result)))
+              (should (equal "src/Component/Foo.idr" (cdr result)))))
+
+        (advice-remove 'idris-ipkg-find-src-dir #'idris-ipkg-find-src-dir-stub)
+        (advice-remove 'idris-find-file-upwards #'idris-find-file-upwards-stub)
+        (advice-remove 'buffer-file-name #'buffer-file-name-stub)))))
+
 ;; Tests by Yasuhiko Watanabe
 ;; https://github.com/idris-hackers/idris-mode/pull/537/files
 (idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split idris-test-eq-buffer)