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

Author: jfdm

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,15 +773,15 @@ 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 ()
   "Replace the previous proof search result with the next one, if it exists.
 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))

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."

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)