branch: elpa/idris-mode
commit 9b743421cd530ebc52efd36619dc35b1c2dbb953
Merge: 49c6f3861f7 f25b37b5bde
Author: Jan de Muijnck-Hughes <[email protected]>
Commit: GitHub <[email protected]>
Merge pull request #651 from keram/interactive-user-errors
Use user-error instead of error in interactive functions that are directly
invoked by the user
---
idris-commands.el | 32 ++++++++++++++++----------------
idris-prover.el | 6 +++---
idris-repl.el | 2 +-
3 files changed, 20 insertions(+), 20 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 305e27bb0e7..417c8278809 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -227,7 +227,7 @@ A prefix argument SET-LINE forces loading but only up to
the current line."
(lambda (_condition)
(when (member 'warnings-tree idris-warnings-printing)
(idris-list-compiler-notes))))))
- (error "Cannot find file for current buffer")))
+ (user-error "Cannot find file for current buffer")))
(defun idris-view-compiler-log ()
"Jump to the log buffer, if it is open."
@@ -244,7 +244,7 @@ A prefix argument SET-LINE forces loading but only up to
the current line."
#'(lambda (w1 w2) (<= (overlay-start w1)
(overlay-start w2))))))
(if warnings-forward
(goto-char (overlay-start (car warnings-forward)))
- (error "No warnings or errors until end of buffer"))))
+ (user-error "No warnings or errors until end of buffer"))))
(defun idris-previous-error ()
"Jump to the previous error overlay in the buffer."
@@ -253,7 +253,7 @@ A prefix argument SET-LINE forces loading but only up to
the current line."
#'(lambda (w1 w2) (>= (overlay-end w1)
(overlay-end w2))))))
(if warnings-backward
(goto-char (overlay-end (car warnings-backward)))
- (error "No warnings or errors until beginning of buffer"))))
+ (user-error "No warnings or errors until beginning of buffer"))))
(defun idris-load-file-sync ()
"Pass the current buffer's file synchronously to the inferior Idris process.
@@ -280,7 +280,7 @@ This sets the load position to point, if there is one."
(setq idris-currently-loaded-buffer (current-buffer))
(idris-make-clean)
(idris-update-loaded-region (car result)))))
- (error "Cannot find file for current buffer")))
+ (user-error "Cannot find file for current buffer")))
@@ -512,9 +512,9 @@ Useful for writing papers or slides."
(fmt (completing-read "What format? " '("html", "latex") nil t nil nil
"latex"))
(width (read-string "How wide? " nil nil "80")))
(if (<= (string-to-number width) 0)
- (error "Width must be positive")
+ (user-error "Width must be positive")
(if (< (length what) 1)
- (error "Nothing to pretty-print")
+ (user-error "Nothing to pretty-print")
(let ((text (idris-eval `(:interpret ,(concat ":pprint " fmt " " width
" " what)))))
(with-idris-info-buffer
(insert (car text))
@@ -773,7 +773,7 @@ A plain prefix ARG causes the command to prompt for hints
and recursion
(idris-eval `(:proof-search ,(cdr what) ,(car what)
,hints ,@depth))
))))
(if (string= result "")
- (error "Nothing found")
+ (user-error "Nothing found")
(idris-replace-hole-with result))))))
(defun idris-proof-search-next ()
@@ -781,7 +781,7 @@ A plain prefix ARG causes the command to prompt for hints
and recursion
Idris 2 only."
(interactive)
(if (not proof-region-start)
- (error "You must proof search first before looking for subsequent proof
results")
+ (user-error "You must proof search first before looking for subsequent
proof results")
(let ((result (car (idris-eval `:proof-search-next))))
(if (string= result "No more results")
(message "No more results")
@@ -805,7 +805,7 @@ Idris 2 only."
final-point
(prefix (idris-line-indentation-for what)))
(if (string= result "")
- (error "Nothing found")
+ (user-error "Nothing found")
(beginning-of-line)
(forward-line)
(while (and (not (eobp))
@@ -825,7 +825,7 @@ Idris 2 only."
Idris 2 only."
(interactive)
(if (not def-region-start)
- (error "You must program search first before looking for subsequent
program results")
+ (user-error "You must program search first before looking for subsequent
program results")
(let ((result (car (idris-eval `:generate-def-next))))
(if (string= result "No more results")
(message "No more results")
@@ -841,7 +841,7 @@ Idris 2 only."
(interactive)
(let ((what (idris-thing-at-point)))
(unless (car what)
- (error "Could not find a hole at point to refine by"))
+ (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))))))
(pcase results
@@ -853,7 +853,7 @@ Idris 2 only."
(interactive "MRefine by: ")
(let ((what (idris-thing-at-point)))
(unless (car what)
- (error "Could not find a hole at point to refine by"))
+ (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)))))
(idris-replace-hole-with result))))
@@ -1015,7 +1015,7 @@ performed silently without confirmation from the user."
(ibc (concat (file-name-sans-extension fname) ".ibc")))
(if (not (member (file-name-extension fname)
'("idr" "lidr" "org" "markdown" "md")))
- (error "The current file is not an Idris file")
+ (user-error "The current file is not an Idris file")
(when (or no-confirmation (y-or-n-p (concat "Really delete " ibc "?")))
(when (file-exists-p ibc)
(delete-file ibc)
@@ -1027,7 +1027,7 @@ performed silently without confirmation from the user."
It is an error if POS is not in the specified term. TERM should
be Idris's own serialization of the term in question."
(unless (equal (get-char-property pos 'idris-tt-term) term)
- (error "Term not present at %s" pos))
+ (user-error "Term not present at %s" pos))
(save-excursion
;; Find the beginning of the active term
(goto-char pos)
@@ -1260,7 +1260,7 @@ of the term to replace."
(interactive)
(let ((files (idris-find-file-upwards "ipkg")))
(cond ((= (length files) 0)
- (error "No .ipkg file found"))
+ (user-error "No .ipkg file found"))
((= (length files) 1)
(find-file (car files)))
(t (find-file (completing-read "Package file: " files nil t))))))
@@ -1280,7 +1280,7 @@ of the term to replace."
(first-mod (read-string
(format "First module name (%s): " module-name-suggestion)
nil nil module-name-suggestion)))
- (when (file-exists-p create-in) (error "%s already exists" create-in))
+ (when (file-exists-p create-in) (user-error "%s already exists" create-in))
(when (string= src-dir "") (setq src-dir nil))
(make-directory create-in t)
(when src-dir (make-directory (concat (file-name-as-directory create-in)
src-dir) t))
diff --git a/idris-prover.el b/idris-prover.el
index 57004a26196..b148c8450f0 100644
--- a/idris-prover.el
+++ b/idris-prover.el
@@ -204,7 +204,7 @@ Tactics are required to begin at the left margin."
(next-tactic (idris-prover-find-tactic
idris-prover-script-processed)))
(if (null next-tactic)
- (error "At the end of the proof script")
+ (user-error "At the end of the proof script")
(let* ((tactic-start (car next-tactic))
(tactic-end (cdr next-tactic))
(tactic-text (buffer-substring-no-properties tactic-start
@@ -267,7 +267,7 @@ Tactics are required to begin at the left margin."
#'(lambda (_result) t)
#'(lambda (condition)
(message (concat idris-prover-error-message-prefix
condition))))
- (error "No proof in progress")))
+ (user-error "No proof in progress")))
(easy-menu-define idris-prover-script-mode-menu idris-prover-script-mode-map
"Menu for Idris prover scripts."
@@ -374,7 +374,7 @@ the length reported by Idris."
(yes-or-no-p "Abandon proof and discard script? "))
(if idris-prover-currently-proving
(idris-eval (list :interpret (if idris-enable-elab-prover ":abandon"
"abandon")) t)
- (error "No proof in progress"))))
+ (user-error "No proof in progress"))))
(defun idris-prover-end ()
"Remove buffers from proof mode and unset global state related to the
prover."
diff --git a/idris-repl.el b/idris-repl.el
index 785881d4305..aa5fbadd88c 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -612,7 +612,7 @@ files and this function is sufficient."
(let ((file (or filename (idris-repl-history-file-f)))
(hist (or history idris-repl-input-history)))
(unless (file-writable-p file)
- (error (format "History file not writable: %s" file)))
+ (user-error (format "History file not writable: %s" file)))
(let ((hist (cl-subseq hist 0 (min (length hist)
idris-repl-history-size))))
(with-temp-file file
(let ((cs idris-repl-history-file-coding-system)
