Simplify idris-generate-def, remove dead code and

add test for `idris-generate-def-next`
Also remove uncessary backtick

Author: keram

idris-commands.el

@@ -785,15 +785,15 @@ Idris 2 only."
             (prefix (save-excursion
                       (goto-char (point-min))
                       (forward-line (1- (cdr what)))
-                      (goto-char (line-beginning-position))
+                      (beginning-of-line)
                       (re-search-forward "\\(^>?\\s-*\\)" nil t)
                       (or (match-string 1) ""))))
         (if (string= result "")
             (error "Nothing found")
-          (goto-char (line-beginning-position))
+          (beginning-of-line)
           (forward-line)
           (while (and (not (eobp))
-                      (progn (goto-char (line-beginning-position))
+                      (progn (beginning-of-line)
                              (looking-at-p (concat prefix "\\s-+"))))
             (forward-line))
           (insert prefix)
@@ -803,11 +803,6 @@ Idris 2 only."
           (setq def-region-end (point))
           (newline)
           (goto-char final-point)
-;          (save-excursion
-;            (forward-line 1)
-;            (setq def-region-start (point))
-;            (insert result)
-;            (setq def-region-end (point)))
           )))))
 
 (defun idris-generate-def-next ()
@@ -816,7 +811,7 @@ Idris 2 only."
   (interactive)
   (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))))
+    (let ((result (car (idris-eval :generate-def-next))))
       (if (string= result "No more results")
           (message "No more results")
         (save-excursion

test/idris-commands-test.el

@@ -574,6 +574,104 @@ Matrix i j = i ?hole2"
       (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
       (advice-remove 'idris-eval #'idris-eval-stub))))
 
+(ert-deftest idris-generate-def ()
+  "Test `idris-generate-def'."
+  (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
+        (progn
+          ;; hapy path
+          (with-temp-buffer
+            (insert "data Foo = A | B
+
+testf : Foo -> Int
+")
+            (goto-char (point-min))
+            (re-search-forward "test")
+            (let ((eval-result (list #'identity '("testf A = testf B\ntestf B = testf A"))))
+              (funcall-interactively 'idris-generate-def))
+            ;; (message (buffer-substring-no-properties (point-min) (point-max)))
+            (should (string= "data Foo = A | B
+
+testf : Foo -> Int
+testf A = testf B
+testf B = testf A
+"
+                             (buffer-substring-no-properties (point-min) (point-max)))))
+          ;; sad path
+          (with-temp-buffer
+            (insert "data Foo = A | B
+
+testf : Foo -> Int
+")
+            (goto-char (point-min))
+            (re-search-forward "test")
+            (let ((eval-result (list #'identity '(""))))
+              (should-error
+               (funcall-interactively 'idris-generate-def))))
+
+          ;; sad path 2
+          (with-temp-buffer
+            (insert "data Foo = A | B
+
+testf : Foo -> Int
+")
+            (goto-char (point-min))
+            (re-search-forward "test")
+            (let ((eval-result (list #'error "%s (synchronous Idris evaluation failed)" "Nothing found")))
+              (should-error
+               (funcall-interactively 'idris-generate-def)))))
+
+      (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+      (advice-remove 'idris-eval #'idris-eval-stub))))
+
+(ert-deftest idris-generate-def-next ()
+  "Test `idris-generate-def-next'."
+  (skip-unless (string-match-p "idris2$" idris-interpreter-path))
+  (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
+        (progn
+          (with-temp-buffer
+            (insert "data Foo = A | B
+
+testf : Foo -> Int
+")
+            (goto-char (point-min))
+            (re-search-forward "test")
+            (let ((eval-result (list #'identity '("testf A = testf B\ntestf B = testf A"))))
+              (funcall-interactively 'idris-generate-def))
+
+            (let ((eval-result (list #'identity '("testf A = 1\ntestf B = 2"))))
+              (funcall-interactively 'idris-generate-def-next))
+            (should (string= "data Foo = A | B
+
+testf : Foo -> Int
+testf A = 1
+testf B = 2
+"
+                             (buffer-substring-no-properties (point-min) (point-max))))
+
+            (let ((eval-result (list #'identity '("third definition"))))
+              (funcall-interactively 'idris-generate-def-next))
+            (should (string= "data Foo = A | B
+
+testf : Foo -> Int
+third definition
+"
+                             (buffer-substring-no-properties (point-min) (point-max))))
+            (let ((eval-result (list #'error "%s (synchronous Idris evaluation failed)" "No more results")))
+              (should-error (funcall-interactively 'idris-generate-def-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)