branch: elpa/idris-mode
commit 6396e1bd8c55b4a34ccddb0a1c8e741873eb8650
Author: Marek L <[email protected]>
Commit: Marek L <[email protected]>
Add accidentaly removed marks for proof-region to
make `idris-proof-search-next` work again.
This was regression introduced in
https://github.com/idris-hackers/idris-mode/pull/578
---
idris-commands.el | 14 ++++++++------
test/idris-commands-test.el | 33 +++++++++++++++++++++++++++++++++
2 files changed, 41 insertions(+), 6 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 417c827880..e7f611224c 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -734,6 +734,11 @@ If no indentation is found, return the empty string."
(idris-repl-eval-string (format ":exec %s" name) 0))
(idris-eval '(:interpret ":exec"))))
+(defvar-local proof-region-start nil
+ "The start position of the last proof region.")
+(defvar-local proof-region-end nil
+ "The end position of the last proof region.")
+
(defun idris-replace-hole-with (expr)
"Replace the hole under the cursor by some EXPR."
(save-excursion
@@ -741,12 +746,9 @@ If no indentation is found, return the empty string."
(end (progn (forward-char) (search-forward-regexp "[^a-zA-Z0-9_']")
(backward-char) (point))))
(delete-region start end))
- (insert expr)))
-
-(defvar-local proof-region-start nil
- "The start position of the last proof region.")
-(defvar-local proof-region-end nil
- "The end position of the last proof region.")
+ (setq proof-region-start (point))
+ (insert expr)
+ (setq proof-region-end (point))))
(defun idris-proof-search (&optional arg)
"Invoke the proof search.
diff --git a/test/idris-commands-test.el b/test/idris-commands-test.el
index f1d42af1e1..7026fe9b50 100644
--- a/test/idris-commands-test.el
+++ b/test/idris-commands-test.el
@@ -544,6 +544,39 @@ third definition
(advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
(advice-remove 'idris-eval #'idris-eval-stub)))))
+(ert-deftest idris-proof-search-next ()
+ "Test `idris-proof-search-next'."
+ (skip-unless (string-match-p "idris2$" idris-interpreter-path))
+ (let (eval-result)
+ (cl-flet ((idris-load-file-sync-stub () nil)
+ (idris-eval-stub (sexp &optional no-errors)
+ (apply #'funcall eval-result)))
+ (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+ (advice-add 'idris-eval :override #'idris-eval-stub)
+ (unwind-protect
+ (with-temp-buffer
+ (insert "data Foo = A | B
+
+testf : Foo -> Int
+testf x = ?hole1
+")
+ (goto-char (point-min))
+ (re-search-forward "hole")
+ (setq eval-result (list #'identity '("42")))
+ (funcall-interactively 'idris-proof-search)
+ (should (string-match-p "testf x = 42"
+ (buffer-substring-no-properties
(point-min) (point-max))))
+ (setq eval-result (list #'identity '("1337")))
+ (funcall-interactively 'idris-proof-search-next)
+ (should (string-match-p "testf x = 1337"
+ (buffer-substring-no-properties
(point-min) (point-max))))
+
+ (setq eval-result (list #'error "%s (synchronous Idris evaluation
failed)" "No more results"))
+ (should-error (funcall-interactively 'idris-proof-search-next)))
+
+ (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+ (advice-remove 'idris-eval #'idris-eval-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)
