search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Fix failure to find beginning of function type definition #562

Closed keram closed 1 year ago

keram commented 1 year ago

when lifting hole and function name contains underscore. Previously in such case the M-x make-lemma command ends with:

Test idris-make-lemma/test-data/MakeLemma condition:
    (search-failed "^\\(\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:")

Tested with Idris 1.3.3 and Idris 2

We may probably at some point need to update regexps https://github.com/idris-hackers/idris-mode/blob/main/idris-commands.el#L732-L733 but as we do not have tests for that scenario and I don't know yet how to test that manually, saving that for later.

jfdm commented 1 year ago

thanks!