Skip to content

Commit

Permalink
Merge pull request #569 from keram/idris2-mode-issues-16
Browse files Browse the repository at this point in the history
Consider `-` as operator in `idris-thing-at-point`
  • Loading branch information
jfdm committed Dec 1, 2022
2 parents 0093e0b + f3a032c commit d08fd3e
Show file tree
Hide file tree
Showing 3 changed files with 33 additions and 5 deletions.
9 changes: 6 additions & 3 deletions idris-commands.el
Original file line number Diff line number Diff line change
Expand Up @@ -326,14 +326,17 @@ Idris process. This sets the load position to point, if there is one."
(error "Cannot find file for current buffer")))


(defun idris-operator-at-position-p (pos)
"Return t if syntax lookup is `.' or char after POS is `-'."
(or (equal (syntax-after pos) (string-to-syntax "."))
(eq (char-after pos) ?-)))

(defun idris-thing-at-point ()
"Return the line number and name at point as a cons.
Use this in Idris source buffers."
(let ((line (idris-get-line-num (point))))
(cons
(if (equal (syntax-after (point))
(string-to-syntax "."))
;; We're on an operator.
(if (idris-operator-at-position-p (point))
(save-excursion
(skip-syntax-backward ".")
(let ((beg (point)))
Expand Down
23 changes: 23 additions & 0 deletions idris-tests.el
Original file line number Diff line number Diff line change
Expand Up @@ -177,5 +177,28 @@ remain."
(kill-buffer buffer))
(idris-quit)))

(ert-deftest idris-test-idris-add-clause ()
"Test that `idris-add-clause' generates definition with hole."
(let ((buffer (find-file "test-data/AddClause.idr"))
(buffer-content (with-temp-buffer
(insert-file-contents "AddClause.idr")
(buffer-string))))
(with-current-buffer buffer
(goto-char (point-min))
(re-search-forward "test :")
(goto-char (match-beginning 0))
(funcall-interactively 'idris-add-clause nil)
(should (looking-at-p "test \\w+ = \\?test_rhs"))
(re-search-forward "(-) :")
(goto-char (1+ (match-beginning 0)))
(funcall-interactively 'idris-add-clause nil)
(should (looking-at-p "(-) = \\?\\w+_rhs"))
;; Cleanup
(erase-buffer)
(insert buffer-content)
(save-buffer)
(kill-buffer)))
(idris-quit))

(provide 'idris-tests)
;;; idris-tests.el ends here
6 changes: 4 additions & 2 deletions test-data/AddClause.idr
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ data Test = A | B

--++++++++++++++++
test : Test -> Int
test x = ?test_rhs


-- Regression test for:
-- idris-add-clause doesn't send a message when cursor is on a dash
-- https://github.com/idris-community/idris2-mode/issues/16
(-) : Nat

0 comments on commit d08fd3e

Please sign in to comment.