branch: elpa/idris-mode
commit 253e2ad90985c83c5cb06bae0b1cb931c88a6c89
Merge: a060688b5c 7697b8b95e
Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com>
Commit: GitHub <nore...@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
