emacs-elpa-diffs
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[nongnu] elpa/idris-mode 5b3c88dc1d 11/18: Add test for idris-refine


From: ELPA Syncer
Subject: [nongnu] elpa/idris-mode 5b3c88dc1d 11/18: Add test for idris-refine
Date: Thu, 8 Dec 2022 05:59:07 -0500 (EST)

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

    Add test for idris-refine
---
 idris-tests.el       | 25 +++++++++++++++++++++++++
 test-data/Refine.idr |  4 ----
 2 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/idris-tests.el b/idris-tests.el
index a042a5d61d..5bc9d5153f 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -203,6 +203,31 @@ remain."
       (kill-buffer))
     (idris-quit)))
 
+(ert-deftest idris-test-idris-refine ()
+  "Test that `idris-refine' works as expected."
+  (let* ((buffer (find-file "test-data/Refine.idr"))
+         (buffer-content (buffer-substring-no-properties (point-min) 
(point-max))))
+    (goto-char (point-min))
+    (search-forward "test : T")
+    (beginning-of-line)
+    (funcall-interactively 'idris-add-clause nil)
+    (should (looking-at-p "test \\w+ = \\?test_rhs"))
+    (idris-delete-ibc t)
+    (search-forward "?test")
+    (funcall-interactively 'idris-refine "x")
+    (should (looking-at-p
+             (if (>=-protocol-version 2 1)
+                 "x"
+               "?test_rhs1")))
+    (idris-delete-ibc t)
+    ;; Cleanup
+    ;; (sit-for 3) ;; usefull for manual inspection before restore
+    (erase-buffer)
+    (insert buffer-content)
+    (save-buffer)
+    (kill-buffer)
+    (idris-quit)))
+
 (ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
   "Test idris-backard-toplevel navigation command."
   (idris-test-with-temp-buffer
diff --git a/test-data/Refine.idr b/test-data/Refine.idr
index 7f90b68517..1a2b830821 100644
--- a/test-data/Refine.idr
+++ b/test-data/Refine.idr
@@ -8,7 +8,3 @@ f : Test -> Test
 f = const A
 
 test : Test -> Test
-
-
-
-



reply via email to

[Prev in Thread] Current Thread [Next in Thread]