[nongnu] elpa/idris-mode ac029bc67e 06/12: Trim left whitespace from Idris add-clause response

[ELPA Syncer]

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

    Trim left whitespace from Idris add-clause response
    
    Why:
    Idris2 returns generated string with indentation and as
    we compute the indentation ourself the result ends inserted
    with extra space.
---
 idris-commands.el |  2 +-
 idris-tests.el    | 18 ++++++++++++++++--
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index c1c8f3bfcd..44eda92763 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -618,7 +618,7 @@ Otherwise, case split as a pattern variable."
         (command (if proof :add-proof-clause :add-clause)))
     (when (car what)
       (save-excursion (idris-load-file-sync))
-      (let ((result (car (idris-eval `(,command ,(cdr what) ,(car what)))))
+      (let ((result (string-trim-left (car (idris-eval `(,command ,(cdr what) 
,(car what))))))
             final-point
             (prefix (save-excursion        ; prefix is the indentation to 
insert for the clause
                       (goto-char (point-min))
diff --git a/idris-tests.el b/idris-tests.el
index 5bc9d5153f..1020030b3a 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -179,9 +179,9 @@ remain."
 
 (ert-deftest idris-test-idris-add-clause ()
   "Test that `idris-add-clause' generates definition with hole."
-  (let ((buffer (find-file "test-data/AddClause.idr"))
+  (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
         (buffer-content (with-temp-buffer
-                          (insert-file-contents "AddClause.idr")
+                          (insert-file-contents "test-data/AddClause.idr")
                           (buffer-string))))
     (with-current-buffer buffer
       (goto-char (point-min))
@@ -195,6 +195,20 @@ remain."
       (goto-char (1+ (match-beginning 0)))
       (funcall-interactively 'idris-add-clause nil)
       (should (looking-at-p "(-) = \\?\\w+_rhs"))
+      (idris-delete-ibc t)
+
+      ;; Test that response with indentation (Idris2) are aligned correctly
+      ;; Idris1 response: "revAcc xs ys = ?revAcc_rhs"
+      ;; Idris2 response: "  revAcc xs ys = ?revAcc_rhs"
+      (goto-char (point-max))
+      (insert "
+myReverse : List a -> List a
+myReverse xs = revAcc [] xs where
+  revAcc : List a -> List a -> List a")
+      (search-backward "evAcc")
+      (funcall-interactively 'idris-add-clause nil)
+      (beginning-of-line)
+      (should (looking-at-p "^  revAcc xs ys = \\?revAcc_rhs"))
 
       ;; Cleanup
       (erase-buffer)