[nongnu] elpa/idris-mode 253e2ad909 5/5: Merge pull request #605 from keram/print-def

[ELPA Syncer]

branch: elpa/idris-mode
commit 253e2ad90985c83c5cb06bae0b1cb931c88a6c89
Merge: a060688b5c 7697b8b95e
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #605 from keram/print-def
    
    Add support for printing definitions of functions in Idris 2
---
 idris-commands.el     | 32 ++++++++++++++++++++++----------
 idris-common-utils.el |  2 +-
 2 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index 88f5c590ab..4cfe3489eb 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -283,9 +283,9 @@ This sets the load position to point, if there is one."
 
 
 
-(defun idris-info-for-name (what name)
-  "Display the type for a NAME."
-  (let* ((ty (idris-eval (list what name)))
+(defun idris-info-for-name (command name)
+  "Pass to Idris compiler COMMAND with NAME as argument and display the 
result."
+  (let* ((ty (idris-eval (list command name)))
              (result (car ty))
              (formatting (cdr ty)))
       (idris-show-info (format "%s" result) formatting)))
@@ -301,13 +301,25 @@ This sets the load position to point, if there is one."
     (when name
       (idris-info-for-name :type-of name))))
 
-(defun idris-print-definition-of-name (thing)
-  "Display the definition of the function or type of the THING at point."
+(defun idris--print-definition-of-name (name)
+  "Fetch from the Idris compiler and display the definition of the NAME."
+  (if (>=-protocol-version 2 1)
+      (idris-info-for-name :interpret (concat ":printdef " name))
+    (idris-info-for-name :print-definition name)))
+
+(defun idris-print-definition-of-name-at-point (name)
+  "Display the definition of the function or type of the NAME at point.
+
+Idris 2 as of 05/01/2023 does not yet fully support
+printing definition of a type at point."
   (interactive "P")
-  (let ((name (if thing (read-string "Print definition: ")
-                (idris-name-at-point))))
-    (when name
-      (idris-info-for-name :print-definition name))))
+  (let ((name* (if name
+                   (read-string "Print definition: ")
+                 (idris-name-at-point))))
+    (when name*
+      (idris--print-definition-of-name name*))))
+
+(define-obsolete-function-alias 'idris-print-definition-of-name 
'idris-print-definition-of-name-at-point "2023-01-05")
 
 (defun idris-who-calls-name (name)
   "Show the callers of NAME in a tree."
@@ -1319,7 +1331,7 @@ of the term to replace."
                        (list "Get definition"
                              (lambda ()
                                (interactive)
-                               (idris-info-for-name :print-definition ref)))
+                               (idris--print-definition-of-name ref)))
                        (list "Who calls?"
                              (lambda ()
                                (interactive)
diff --git a/idris-common-utils.el b/idris-common-utils.el
index 3b18bbfc32..e80c31c638 100644
--- a/idris-common-utils.el
+++ b/idris-common-utils.el
@@ -293,7 +293,7 @@ inserted text (that is, relative to point prior to 
insertion)."
             (if term
                 (list 'idris-tt-term (cadr term))
               ())
-            (if key
+            (if (and key (not (string-empty-p (cadr key))))
                 (list 'idris-name-key (concat "{{{{{" (cadr key) "}}}}}"))
               ())
             (if idris-err