[nongnu] elpa/idris-mode 9a4a9641b9 10/18: [ new ] intro command - backport from idris2-mode

[ELPA Syncer]

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

    [ new ] intro command - backport from idris2-mode
    
    https://github.com/idris-community/idris2-mode/pull/21
    
    Updated with suggested key binding by Ohad
    
    Co-authored-by: "G. Allais" <guillaume.allais@ens-lyon.org>
    Co-authored-by: "Ohad Kammar" <ohad.kammar@ed.ac.uk>
---
 idris-commands.el | 35 +++++++++++++++++++++++------------
 idris-keys.el     |  3 ++-
 2 files changed, 25 insertions(+), 13 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index 54f3d1cc55..bce1cfedd9 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -738,6 +738,15 @@ Otherwise, case split as a pattern variable."
         (idris-repl-eval-string (format ":exec %s" name) 0))
     (idris-eval '(:interpret ":exec"))))
 
+(defun idris-replace-hole-with (expr)
+  "Replace the hole under the cursor by some EXPR."
+  (save-excursion
+    (let ((start (progn (search-backward "?") (point)))
+          (end (progn (forward-char) (search-forward-regexp "[^a-zA-Z0-9_']")
+                      (backward-char) (point))))
+      (delete-region start end))
+    (insert expr)))
+
 (defvar-local proof-region-start nil
   "The start position of the last proof region.")
 (defvar-local proof-region-end nil
@@ -769,13 +778,7 @@ prefix argument sets the recursion depth directly."
                            ))))
         (if (string= result "")
             (error "Nothing found")
-          (save-excursion
-            (let ((start (progn (search-backward "?") (point)))
-                  (end (progn (forward-char) (search-forward-regexp 
"[^a-zA-Z0-9_']") (backward-char) (point))))
-              (delete-region start end))
-            (setq proof-region-start (point))
-            (insert result)
-            (setq proof-region-end (point))))))))
+          (idris-replace-hole-with result))))))
 
 (defun idris-proof-search-next ()
   "Replace the previous proof search result with the next one, if it exists.
@@ -851,6 +854,18 @@ Idris 2 only."
           (insert result)
           (setq def-region-end (point)))))))
 
+(defun idris-intro ()
+  "Introduce the unambiguous constructor to use in this hole."
+  (interactive)
+  (let ((what (idris-thing-at-point)))
+    (unless (car what)
+      (error "Could not find a hole at point to refine by"))
+    (save-excursion (idris-load-file-sync))
+    (let ((results (car (idris-eval `(:intro ,(cdr what) ,(car what))))))
+      (pcase results
+        (`(,result) (idris-replace-hole-with result))
+        (_ (idris-replace-hole-with (ido-completing-read "I'm hesitating 
between: " results)))))))
+
 (defun idris-refine (name)
   "Refine by some NAME, without recursive proof search."
   (interactive "MRefine by: ")
@@ -859,11 +874,7 @@ Idris 2 only."
       (error "Could not find a hole at point to refine by"))
     (save-excursion (idris-load-file-sync))
     (let ((result (car (idris-eval `(:refine ,(cdr what) ,(car what) ,name)))))
-      (save-excursion
-        (let ((start (progn (search-backward "?") (point)))
-              (end (progn (forward-char) (search-forward-regexp 
"[^a-zA-Z0-9_']") (backward-char) (point))))
-          (delete-region start end))
-        (insert result)))))
+      (idris-replace-hole-with result))))
 
 (defun idris-identifier-backwards-from-point ()
   (let (identifier-start
diff --git a/idris-keys.el b/idris-keys.el
index ca0e568fbd..7dc5b97027 100644
--- a/idris-keys.el
+++ b/idris-keys.el
@@ -64,7 +64,8 @@
   (define-key map (kbd "C-c C-g") 'idris-generate-def)
   (define-key map (kbd "C-c C-S-g") 'idris-generate-def-next)
 
-  (define-key map (kbd "C-c C-r") 'idris-refine)
+  (define-key map (kbd "C-c C-r") 'idris-intro)
+  (define-key map (kbd "C-c C-S-r") 'idris-refine)
   (define-key map (kbd "RET") 'idris-newline-and-indent)
   ;; Not using `kbd' due to oddness about backspace and delete
   (define-key map [delete] 'idris-delete-forward-char)