idris2-add-clause doesn't send a message when cursor is on a dash (-)
#16
Comments
keram
added a commit
to keram/idris-mode
that referenced
this issue
Nov 25, 2022
Why: The `-` char is defined in idris-syntax-table as being beginning of comment and causing condition: `(equal (syntax-after (point)) (string-to-syntax ".")` in `idris-thing-at-point` be evaluated to nil (false) and throw error. Fixes: idris-community/idris2-mode#16
keram
added a commit
to keram/idris-mode
that referenced
this issue
Nov 26, 2022
Why: The `-` char is defined in idris-syntax-table as being beginning of comment and causing condition: `(equal (syntax-after (point)) (string-to-syntax ".")` in `idris-thing-at-point` be evaluated to nil (false) and throw error. Fixes: idris-community/idris2-mode#16
keram
added a commit
to keram/idris-mode
that referenced
this issue
Nov 26, 2022
Why: The `-` char is defined in idris-syntax-table as being beginning of comment and causing condition: `(equal (syntax-after (point)) (string-to-syntax ".")` in `idris-thing-at-point` be evaluated to nil (false) and throw error. Fixes: idris-community/idris2-mode#16
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Put the cursor on either of the minus signs (line 1 and line 3).
Hit (C-c C-s)
Expected behaviour
Add a stub definition.
Actual behaviour
Nothing, no messages are sent over the connection.
Moving the curosr to a non-dash character (the pipe or the plus in line 3), this command does send a message and the correct definition is generated.
The text was updated successfully, but these errors were encountered: