[nongnu] elpa/idris-mode 486be1b740 1/2: Improve `idris-case-dwim` to make case expression from hole

[ELPA Syncer]

branch: elpa/idris-mode
commit 486be1b740e0fa120fe048e5a8eb00f6661910e8
Author: Marek L <nospam.keram@gmail.com>
Commit: Marek L <nospam.keram@gmail.com>

    Improve `idris-case-dwim` to make case expression from hole
    
    in edge-cases when:
    - point is at ? in ?hole_rs1
    - point is at char after ? in ?hole_rs1
    
    Resolves:
    https://github.com/idris-hackers/idris-mode/issues/441
---
 idris-commands.el | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index 925cff867f..98cdb4350b 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -629,10 +629,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"