branch: elpa/idris-mode
commit 22cc1bf237428b24de5f4f228db747e93a4ae619
Merge: 5442961d09 a04bf0c317
Author: Jan de Muijnck-Hughes <[email protected]>
Commit: GitHub <[email protected]>
Merge pull request #650 from keram/idris-user-eval
Move call to idris-list-compiler-notes from idris-eval to new helper
function idris-user-eval
---
idris-commands.el | 58 +++++++++++++++++++++++++++++++++----------------------
inferior-idris.el | 13 +++++--------
2 files changed, 40 insertions(+), 31 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index eabdc08686..156e1d8924 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -294,6 +294,8 @@ If NO-ERRORS is passed the warnings from Idris will be
ignored."
(let* ((ty (idris-eval (list command name)))
(result (car ty))
(formatting (cdr ty)))
+ (when (member 'warnings-tree idris-warnings-printing)
+ (idris-list-compiler-notes))
(idris-show-info (format "%s" result) formatting)))
@@ -329,9 +331,9 @@ printing definition of a type at point."
(defun idris-who-calls-name (name)
"Show the callers of NAME in a tree."
- (let* ((callers (idris-eval `(:who-calls ,name)))
+ (let* ((callers (idris-user-eval `(:who-calls ,name)))
(roots (mapcar #'(lambda (c) (idris-caller-tree c :who-calls))
- (car callers))))
+ callers)))
(if (not (null roots))
(idris-tree-info-show-multiple roots "Callers")
(message "The name %s was not found." name))
@@ -346,8 +348,8 @@ printing definition of a type at point."
(defun idris-name-calls-who (name)
"Show the callees of NAME in a tree."
- (let* ((callees (idris-eval `(:calls-who ,name)))
- (roots (mapcar #'(lambda (c) (idris-caller-tree c :calls-who)) (car
callees))))
+ (let* ((callees (idris-user-eval `(:calls-who ,name)))
+ (roots (mapcar #'(lambda (c) (idris-caller-tree c :calls-who))
callees)))
(if (not (null roots))
(idris-tree-info-show-multiple roots "Callees")
(message "The name %s was not found." name))
@@ -520,9 +522,9 @@ Useful for writing papers or slides."
(user-error "Width must be positive")
(if (< (length what) 1)
(user-error "Nothing to pretty-print")
- (let ((text (idris-eval `(:interpret ,(concat ":pprint " fmt " " width
" " what)))))
+ (let ((text (idris-user-eval `(:interpret ,(concat ":pprint " fmt " "
width " " what)))))
(with-idris-info-buffer
- (insert (car text))
+ (insert text)
(goto-char (point-min))
(re-search-forward (if (string= fmt "latex")
"% START CODE\n"
@@ -542,7 +544,7 @@ Useful for writing papers or slides."
(let ((what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
- (let ((result (car (idris-eval `(:case-split ,(cdr what) ,(car what)))))
+ (let ((result (idris-user-eval `(:case-split ,(cdr what) ,(car what))))
(initial-position (point)))
(if (<= (length result) 2)
(message "Can't case split %s" (car what))
@@ -558,7 +560,7 @@ Useful for writing papers or slides."
(let ((what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
- (let ((result (car (idris-eval `(:make-case ,(cdr what) ,(car what))))))
+ (let ((result (idris-user-eval `(:make-case ,(cdr what) ,(car what)))))
(if (<= (length result) 2)
(message "Can't make cases from %s" (car what))
(delete-region (line-beginning-position) (line-end-position))
@@ -607,7 +609,7 @@ If no indentation is found, return the empty string."
(command (if proof :add-proof-clause :add-clause)))
(when (car what)
(idris-load-file-sync)
- (let ((result (string-trim-left (car (idris-eval `(,command ,(cdr what)
,(car what))))))
+ (let ((result (string-trim-left (idris-user-eval `(,command ,(cdr what)
,(car what)))))
final-point
(prefix (idris-line-indentation-for what)))
;; Go forward until we get to a line with equal or less indentation to
@@ -633,7 +635,7 @@ If no indentation is found, return the empty string."
(let ((what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
- (let ((result (car (idris-eval `(:add-missing ,(cdr what) ,(car
what))))))
+ (let ((result (idris-user-eval `(:add-missing ,(cdr what) ,(car what)))))
(forward-line 1)
(insert result)))))
@@ -643,7 +645,7 @@ If no indentation is found, return the empty string."
(let ((what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
- (let ((result (car (idris-eval `(:make-with ,(cdr what) ,(car what))))))
+ (let ((result (idris-user-eval `(:make-with ,(cdr what) ,(car what)))))
(beginning-of-line)
(kill-line)
(insert result)))))
@@ -654,7 +656,7 @@ If no indentation is found, return the empty string."
(let ((what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
- (let* ((result (car (idris-eval `(:make-lemma ,(cdr what) ,(car what)))))
+ (let* ((result (idris-user-eval `(:make-lemma ,(cdr what) ,(car what))))
(lemma-type (car result)))
;; There are two cases here: either a ?hole, or the {name} of a
provisional defn.
(cond ((equal lemma-type :metavariable-lemma)
@@ -774,11 +776,9 @@ A plain prefix ARG causes the command to prompt for hints
and recursion
(what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
-
- (let ((result (car (if (> idris-protocol-version 1)
- (idris-eval `(:proof-search ,(cdr what) ,(car
what)))
- (idris-eval `(:proof-search ,(cdr what) ,(car what)
,hints ,@depth))
- ))))
+ (let ((result (idris-user-eval (if (> idris-protocol-version 1)
+ `(:proof-search ,(cdr what) ,(car
what))
+ `(:proof-search ,(cdr what) ,(car what)
,hints ,@depth)))))
(if (string= result "")
(user-error "Nothing found")
(idris-replace-hole-with result))))))
@@ -789,7 +789,7 @@ Idris 2 only."
(interactive)
(if (not proof-region-start)
(user-error "You must proof search first before looking for subsequent
proof results")
- (let ((result (car (idris-eval `:proof-search-next))))
+ (let ((result (idris-user-eval `:proof-search-next)))
(save-excursion
(goto-char proof-region-start)
(delete-region proof-region-start proof-region-end)
@@ -806,7 +806,7 @@ Idris 2 only."
(let ((what (idris-thing-at-point)))
(when (car what)
(idris-load-file-sync)
- (let ((result (car (idris-eval `(:generate-def ,(cdr what) ,(car
what)))))
+ (let ((result (idris-user-eval `(:generate-def ,(cdr what) ,(car what))))
final-point
(prefix (idris-line-indentation-for what)))
(if (string= result "")
@@ -831,7 +831,7 @@ Idris 2 only."
(interactive)
(if (not def-region-start)
(user-error "You must program search first before looking for subsequent
program results")
- (let ((result (car (idris-eval `:generate-def-next))))
+ (let ((result (idris-user-eval `:generate-def-next)))
(save-excursion
(goto-char def-region-start)
(delete-region def-region-start def-region-end)
@@ -846,7 +846,7 @@ Idris 2 only."
(unless (car what)
(user-error "Could not find a hole at point to refine by"))
(idris-load-file-sync)
- (let ((results (car (idris-eval `(:intro ,(cdr what) ,(car what))))))
+ (let ((results (idris-user-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)))))))
@@ -858,7 +858,7 @@ Idris 2 only."
(unless (car what)
(user-error "Could not find a hole at point to refine by"))
(idris-load-file-sync)
- (let ((result (car (idris-eval `(:refine ,(cdr what) ,(car what) ,name)))))
+ (let ((result (idris-user-eval `(:refine ,(cdr what) ,(car what) ,name))))
(idris-replace-hole-with result))))
(defun idris-identifier-backwards-from-point ()
@@ -913,7 +913,7 @@ type-correct, so loading will fail."
(interactive)
(when (idris-current-buffer-dirty-p)
(idris-load-file-sync))
- (idris-hole-list-show (car (idris-eval '(:metavariables 80)))))
+ (idris-hole-list-show (idris-user-eval '(:metavariables 80))))
(defun idris-list-compiler-notes ()
"Show the compiler notes in tree view."
@@ -1406,5 +1406,17 @@ of the term to replace."
(idris-show-core-term
(idris--active-term-beginning tt-term pos)))))))))))
+(defun idris-user-eval (what &optional no-errors)
+ "Send WHAT to Idris process and return first item in the response.
+
+When `idris-warnings-printing' includes `warnings-tree' it also
+ calls `idris-list-compiler-notes' to display or update existing Idris notes.
+
+If `NO-ERRORS' is non-nil, don't raise `ERROR' if there was an Idris error."
+ (let ((ty (idris-eval what no-errors)))
+ (when (member 'warnings-tree idris-warnings-printing)
+ (idris-list-compiler-notes))
+ (car ty)))
+
(provide 'idris-commands)
;;; idris-commands.el ends here
diff --git a/inferior-idris.el b/inferior-idris.el
index 18b330a3e8..44a64e675c 100644
--- a/inferior-idris.el
+++ b/inferior-idris.el
@@ -305,11 +305,9 @@ versions cannot deal with that."
(defvar idris-stack-eval-tags nil
"List of stack-tags of continuations waiting on the stack.")
-(autoload 'idris-list-compiler-notes "idris-commands.el")
(defun idris-eval (sexp &optional no-errors)
"Evaluate SEXP on the inferior Idris and return the result.
-If `NO-ERRORS' is non-nil, don't trigger warning buffers and
- don't call `ERROR' if there was an Idris error."
+If `NO-ERRORS' is non-nil, don't call `ERROR' if there was an Idris error."
(let* ((tag (gensym (format "idris-result-%d-"
(1+ idris-continuation-counter))))
(idris-stack-eval-tags (cons tag idris-stack-eval-tags)))
@@ -326,11 +324,10 @@ If `NO-ERRORS' is non-nil, don't trigger warning buffers
and
(error "Reply to canceled synchronous eval request tag=%S
sexp=%S"
tag sexp))))
((:error condition &optional _spans)
- (if no-errors
- (throw tag (list #'identity nil))
- (when (member 'warnings-tree idris-warnings-printing)
- (idris-list-compiler-notes))
- (throw tag (list #'error "%s (synchronous Idris evaluation
failed)" condition)))))
+ (throw tag (if no-errors
+ ;; TODO: better way to communicate error upstream
+ (list #'identity (cons :error condition))
+ (list #'user-error "%s (synchronous Idris evaluation
failed)" condition)))))
(let ((debug-on-quit t)
(inhibit-quit nil))
(while t
