[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/idris-mode 3c3a87c66c 1/6: Fix failure to find beginning o
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/idris-mode 3c3a87c66c 1/6: Fix failure to find beginning of function type definition |
Date: |
Fri, 18 Nov 2022 05:59:08 -0500 (EST) |
branch: elpa/idris-mode
commit 3c3a87c66cba6c16851999ea93002e78245d5a6a
Author: Marek L <nospam.keram@gmail.com>
Commit: Marek L <nospam.keram@gmail.com>
Fix failure to find beginning of function type definition
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-*:")
```
---
idris-commands.el | 4 ++--
test-data/MakeLemma.idr | 6 ++----
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 3645b8ba7d..925cff867f 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -712,8 +712,8 @@ Otherwise, case split as a pattern variable."
;; now we add the type signature - search upwards for the
current
;; signature, then insert before it
(re-search-backward (if (idris-lidr-p)
-
"^\\(>\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:"
-
"^\\(\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:"))
+
"^\\(>\\s-*\\)\\(([^)]+)\\|[a-zA-Z_0-9]+\\)\\s-*:"
+
"^\\(\\s-*\\)\\(([^)]+)\\|[a-zA-Z_0-9]+\\)\\s-*:"))
(let ((indentation (match-string 1)) end-point)
(beginning-of-line)
(insert indentation)
diff --git a/test-data/MakeLemma.idr b/test-data/MakeLemma.idr
index 517e92b93e..d4f86f3d5d 100644
--- a/test-data/MakeLemma.idr
+++ b/test-data/MakeLemma.idr
@@ -3,8 +3,6 @@ module MakeLemma
-- (idris-test-run-goto-char #'idris-make-lemma)
data Test = A | B
-test : Test -> Test
+my_lemmaTest : Test -> Test
-- +++++++++++
-test x = ?make_lemma
-
-
+my_lemmaTest x = ?my_lemmaTest_rhs
- [nongnu] elpa/idris-mode updated (1dc558ad24 -> 67e06eccbd), ELPA Syncer, 2022/11/18
- [nongnu] elpa/idris-mode 8329b73be8 3/6: Move "words of encouragement" from minibuffer to Idris repl banner, ELPA Syncer, 2022/11/18
- [nongnu] elpa/idris-mode 3c3a87c66c 1/6: Fix failure to find beginning of function type definition,
ELPA Syncer <=
- [nongnu] elpa/idris-mode 43e8a6e723 5/6: Merge pull request #564 from keram/fix-encouragement-in-process-buffer, ELPA Syncer, 2022/11/18
- [nongnu] elpa/idris-mode ca860db9ae 4/6: Merge pull request #562 from keram/make-lemma-underscore, ELPA Syncer, 2022/11/18
- [nongnu] elpa/idris-mode 67e06eccbd 6/6: Merge pull request #565 from keram/words-of-encouragement-in-repl-banner, ELPA Syncer, 2022/11/18
- [nongnu] elpa/idris-mode 62c3ad2b0d 2/6: Make empty string always return value from `idris-process-filter`, ELPA Syncer, 2022/11/18