branch: elpa/idris-mode
commit f49254808444022b4c122cee2bd4025dfb605981
Author: Marek L <[email protected]>
Commit: Marek L <[email protected]>
Extract `(car (idris-eval ..` in commands to `idris-user-eval`
This will allow us to:
- globally handle updating idris notes when needed
- remove (cyclic) dependency of `inferior-idris.el` on
`idris-list-compiler-notes`
- remove duplication
- unify and improve response handling
---
idris-commands.el | 53 +++++++++++++++++++++++++++++------------------------
1 file changed, 29 insertions(+), 24 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index a5aaf2a7a4..b8599d6d60 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -271,7 +271,7 @@ This sets the load position to point, if there is one."
(idris-switch-working-directory srcdir)
(idris-toggle-semantic-source-highlighting)
(let ((result
- (idris-eval
+ (idris-user-eval
(if idris-load-to-here
`(:load-file ,fn ,(idris-get-line-num
idris-load-to-here))
`(:load-file ,fn))))
@@ -323,9 +323,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))
@@ -340,8 +340,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))
@@ -514,9 +514,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"
@@ -536,7 +536,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))
@@ -552,7 +552,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))
@@ -601,7 +601,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
@@ -627,7 +627,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)))))
@@ -637,7 +637,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)))))
@@ -648,7 +648,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)
@@ -768,11 +768,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))))))
@@ -783,7 +781,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)
@@ -800,7 +798,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 "")
@@ -825,7 +823,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)
@@ -840,7 +838,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)))))))
@@ -852,7 +850,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 ()
@@ -907,7 +905,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."
@@ -1400,5 +1398,12 @@ 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.
+
+If `NO-ERRORS' is non-nil, don't raise `ERROR' if there was an Idris error."
+ (let ((ty (idris-eval what no-errors)))
+ (car ty)))
+
(provide 'idris-commands)
;;; idris-commands.el ends here
