[nongnu] elpa/idris-mode 3506c39f5e 10/12: Merge pull request #590 from keram/fix-indent-add-clause-idris2

[ELPA Syncer]

branch: elpa/idris-mode
commit 3506c39f5e9bab97f2ae5be2625d601ca81d62ee
Merge: 8a3229cfe9 ac029bc67e
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #590 from keram/fix-indent-add-clause-idris2
    
    Trim left whitespace from Idris add-clause response
---
 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 c068305808..9641255854 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -619,7 +619,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)