[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/idris-mode cc098578fe 1/2: Restore position after case spl
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/idris-mode cc098578fe 1/2: Restore position after case split |
Date: |
Thu, 8 Dec 2022 07:59:05 -0500 (EST) |
branch: elpa/idris-mode
commit cc098578fee8190c0757ac59172114ec66c7eda8
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 f69909c5f5..e1c71da40f 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -567,19 +567,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."
@@ -593,8 +594,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.
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [nongnu] elpa/idris-mode cc098578fe 1/2: Restore position after case split,
ELPA Syncer <=