branch: elpa/idris-mode
commit 281ed4ddc1dc2dc7d0959042a37d9e70fedfaf71
Merge: 21803ac767 5ce410d9c5
Author: Jan de Muijnck-Hughes <[email protected]>
Commit: GitHub <[email protected]>
Merge pull request #669 from keram/fix-proof-next-regression
Make `idris-proof-search-next` work again.
---
idris-commands.el | 42 ++++++++++++++++++++----------------------
test/idris-commands-test.el | 33 +++++++++++++++++++++++++++++++++
2 files changed, 53 insertions(+), 22 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 13df30eebc..a5aaf2a7a4 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -733,6 +733,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
@@ -740,12 +745,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.
@@ -782,14 +784,12 @@ Idris 2 only."
(if (not proof-region-start)
(user-error "You must proof search first before looking for subsequent
proof results")
(let ((result (car (idris-eval `:proof-search-next))))
- (if (string= result "No more results")
- (message "No more results")
- (save-excursion
- (goto-char proof-region-start)
- (delete-region proof-region-start proof-region-end)
- (setq proof-region-start (point))
- (insert result)
- (setq proof-region-end (point)))))))
+ (save-excursion
+ (goto-char proof-region-start)
+ (delete-region proof-region-start proof-region-end)
+ (setq proof-region-start (point))
+ (insert result)
+ (setq proof-region-end (point))))))
(defvar-local def-region-start nil)
(defvar-local def-region-end nil)
@@ -826,14 +826,12 @@ Idris 2 only."
(if (not def-region-start)
(user-error "You must program search first before looking for subsequent
program results")
(let ((result (car (idris-eval `:generate-def-next))))
- (if (string= result "No more results")
- (message "No more results")
- (save-excursion
- (goto-char def-region-start)
- (delete-region def-region-start def-region-end)
- (setq def-region-start (point))
- (insert result)
- (setq def-region-end (point)))))))
+ (save-excursion
+ (goto-char def-region-start)
+ (delete-region def-region-start def-region-end)
+ (setq def-region-start (point))
+ (insert result)
+ (setq def-region-end (point))))))
(defun idris-intro ()
"Introduce the unambiguous constructor to use in this hole."
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)
