From 92b7e1ba10e84635fd7ac5fd5e2e62eb6a6effab Mon Sep 17 00:00:00 2001 From: Marek L 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 +++++++-------- idris-compat.el | 23 +++++++++++++++++++++ test/idris-commands-test.el | 40 +++++++++++++++++++++++++++++++++++++ 3 files changed, 71 insertions(+), 8 deletions(-) diff --git a/idris-commands.el b/idris-commands.el index 95975e1a..a7f3be8b 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 (idris-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/idris-compat.el b/idris-compat.el index d248d7f8..845cfc9e 100644 --- a/idris-compat.el +++ b/idris-compat.el @@ -41,5 +41,28 @@ attention to case differences." (concat (apply 'concat (mapcar 'file-name-as-directory dirs)) (car (reverse components)))))) +(if (fboundp 'file-name-parent-directory) + (defalias 'idris-file-name-parent-directory 'file-name-parent-directory) + ;; Extracted from Emacs 29+ https://github.com/emacs-mirror/emacs/blob/master/lisp/files.el + (defun idris-file-name-parent-directory (filename) + "Return the directory name of the parent directory of FILENAME. +If FILENAME is at the root of the filesystem, return nil. +If FILENAME is relative, it is interpreted to be relative +to `default-directory', and the result will also be relative." + (let* ((expanded-filename (expand-file-name filename)) + (parent (file-name-directory (directory-file-name expanded-filename)))) + (cond + ;; filename is at top-level, therefore no parent + ((or (null parent) + ;; `equal' is enough, we don't need to resolve symlinks here + ;; with `file-equal-p', also for performance + (equal parent expanded-filename)) + nil) + ;; filename is relative, return relative parent + ((not (file-name-absolute-p filename)) + (file-relative-name parent)) + (t + parent))))) + (provide 'idris-compat) ;;; idris-compat.el ends here diff --git a/test/idris-commands-test.el b/test/idris-commands-test.el index 4d1f95e4..7c38bcc7 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)