emacs-elpa-diffs
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[nongnu] elpa/idris-mode 94a88cdb99 07/18: Restore position after case s


From: ELPA Syncer
Subject: [nongnu] elpa/idris-mode 94a88cdb99 07/18: Restore position after case split
Date: Thu, 8 Dec 2022 05:59:07 -0500 (EST)

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

    Restore position after case split
    
    Addresses feedback on https://github.com/idris-hackers/idris-mode/pull/465 
with
    small improvement for making case from hole where the point is moved
    back to position of `_` in `case _ of` as that is place user
    may most likely edit next.
    
    Closes https://github.com/idris-hackers/idris-mode/pull/465
---
 idris-commands.el | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index 54f3d1cc55..5074131425 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -570,19 +570,20 @@ Useful for writing papers or slides."
 
 
 (defun idris-case-split ()
-  "Case split the pattern variable at point"
+  "Case split the pattern variable at point."
   (interactive)
   (let ((what (idris-thing-at-point)))
     (when (car what)
       (save-excursion (idris-load-file-sync))
-      (let ((result (car (idris-eval `(:case-split ,(cdr what) ,(car what))))))
+      (let ((result (car (idris-eval `(:case-split ,(cdr what) ,(car what)))))
+            (initial-position (point)))
         (if (<= (length result) 2)
             (message "Can't case split %s" (car what))
           (delete-region (line-beginning-position) (line-end-position))
           (if (> idris-protocol-version 1)
               (insert (substring result 0 (length result)))
-              (insert (substring result 0 (1- (length result))))
-              ))))))
+            (insert (substring result 0 (1- (length result)))))
+          (goto-char initial-position))))))
 
 (defun idris-make-cases-from-hole ()
   "Make a case expression from the metavariable at point."
@@ -596,8 +597,8 @@ Useful for writing papers or slides."
           (delete-region (line-beginning-position) (line-end-position))
           (if (> idris-protocol-version 1)
               (insert (substring result 0 (length result)))
-              (insert (substring result 0 (1- (length result))))
-              ))))))
+            (insert (substring result 0 (1- (length result)))))
+          (search-backward "_ of\n"))))))
 
 (defun idris-case-dwim ()
   "If point is on a hole name, make it into a case expression.



reply via email to

[Prev in Thread] Current Thread [Next in Thread]