[nongnu] elpa/idris-mode 993c862b7f 2/2: Merge pull request #568 from keram/case-dwin-issue-465

[ELPA Syncer]

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"