[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
-
-
-
-
- [nongnu] elpa/idris-mode 3d460800a4 01/18: Remove unecessary pop or display notes buffer, (continued)
- [nongnu] elpa/idris-mode 3d460800a4 01/18: Remove unecessary pop or display notes buffer, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode a971194d56 14/18: Merge pull request #582 from keram/notes-error-buffer-code-cleanup, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 51caa5f3a5 15/18: Merge pull request #585 from keram/emacs28-and-cache-v3, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 43aead3c46 05/18: Make idris-compiler-notes-list-show more similar with idris-hole-list-show, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 68fe8e115f 06/18: Move idris-list-compiler-notes into idris-commands.el, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 80861674a6 08/18: Debug CI idris2 failure 2 - try retry to wait for idris version in idris-switch-working-directory, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 94a88cdb99 07/18: Restore position after case split, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 888bf9614f 04/18: Make notes buffer special and make the show function similar to holes one, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 063a63b770 17/18: Merge pull request #586 from idris-hackers/revert-583-update-pr-465, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 9a4a9641b9 10/18: [ new ] intro command - backport from idris2-mode, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 5b3c88dc1d 11/18: Add test for idris-refine,
ELPA Syncer <=
- [nongnu] elpa/idris-mode a9d12c89e2 12/18: Add Emacs 28.2 to test matrix and, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode b39a08790e 13/18: Merge pull request #583 from keram/update-pr-465, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 744f773bb4 18/18: Merge pull request #578 from keram/backport-pr-21-intro, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode cab95f1fca 09/18: wip test, ELPA Syncer, 2022/12/08
- [nongnu] elpa/idris-mode 9ebd0a7d26 16/18: Revert "Restore position after case split", ELPA Syncer, 2022/12/08