[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/idris-mode 993c862b7f 2/2: Merge pull request #568 from ke
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/idris-mode 993c862b7f 2/2: Merge pull request #568 from keram/case-dwin-issue-465 |
Date: |
Wed, 23 Nov 2022 08:02:55 -0500 (EST) |
branch: elpa/idris-mode
commit 993c862b7fcc97cca1b825d0acf424c70d72ce36
Merge: cc85f0e138 486be1b740
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>
Merge pull request #568 from keram/case-dwin-issue-465
Improve `idris-case-dwim` to make case expression from hole in edge cases
---
idris-commands.el | 13 +++++++++----
1 file changed, 9 insertions(+), 4 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 340d992d4a..256458d274 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -623,10 +623,15 @@ Useful for writing papers or slides."
"If point is on a hole name, make it into a case expression.
Otherwise, case split as a pattern variable."
(interactive)
- (if (or (looking-at-p "\\?[a-zA-Z_]+")
- (looking-back "\\?[a-zA-Z0-9_]+" nil))
- (idris-make-cases-from-hole)
- (idris-case-split)))
+ (cond
+ ((looking-at-p "\\?[a-zA-Z_]+") ;; point at "?" in ?hole_rs1
+ (forward-char) ;; move from "?" for idris-make-cases-from-hole to work
correctly
+ (idris-make-cases-from-hole))
+ ((or (and (char-equal (char-before) ??) ;; point at "h" in ?hole_rs1
+ (looking-at-p "[a-zA-Z_]+"))
+ (looking-back "\\?[a-zA-Z0-9_]+" nil)) ;; point somewhere afte "?h" in
?hole_rs1
+ (idris-make-cases-from-hole))
+ (t (idris-case-split))))
(defun idris-add-clause (proof)
"Add clauses to the declaration at point"
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [nongnu] elpa/idris-mode 993c862b7f 2/2: Merge pull request #568 from keram/case-dwin-issue-465,
ELPA Syncer <=