diff --git a/idris-common-utils.el b/idris-common-utils.el index 986f0db..3b8b803 100644 --- a/idris-common-utils.el +++ b/idris-common-utils.el @@ -47,7 +47,7 @@ "Working directory of Idris process.") (defvar idris-command-line-option-functions nil - "A list of functions to call to compute the 'command-line' arguments to Idris. + "A list of functions to call to compute the `command-line' arguments to Idris. Each function should take no arguments and return a list of strings that are suitable arguments to `start-process'.") diff --git a/idris-highlight-input.el b/idris-highlight-input.el index 70d9472..bde3eac 100644 --- a/idris-highlight-input.el +++ b/idris-highlight-input.el @@ -118,8 +118,8 @@ See Info node `(elisp)Overlay Properties' to understand how ARGS are used." (defun idris-toggle-semantic-source-highlighting () "Turn on/off semantic highlighting. -This is controled by value of`idris-semantic-source-highlighting' variable. -When the value is 'debug additional checks are performed on received data." +This is controled by value of `idris-semantic-source-highlighting' variable. +When the value is `debug' additional checks are performed on received data." (if idris-semantic-source-highlighting (progn (if (eq idris-semantic-source-highlighting 'debug) diff --git a/idris-repl.el b/idris-repl.el index 4ee01ab..785881d 100644 --- a/idris-repl.el +++ b/idris-repl.el @@ -276,7 +276,22 @@ Invokes `idris-repl-mode-hook'." t) (`(:warning ,output ,_target) (when (member 'warnings-repl idris-warnings-printing) - (idris-repl-write-string (format "Error: %s line %d (col %d):\n%s" (nth 0 output) (nth 1 output) (if (eq (safe-length output) 3) 0 (nth 2 output)) (car (last output)))))) + (pcase output + (`(,fname (,start-line ,start-col) (,_end-line ,_end-col) ,msg ,_spans) + (idris-repl-write-string (format "Error: %s line %d (col %d):\n%s" + fname + (1+ start-line) + (1+ start-col) + msg))) + ;; Keeping this old format for backward compatibility. + ;; Probably we can remove it at some point. + (_ (idris-repl-write-string (format "Error: %s line %d (col %d):\n%s" + (nth 0 output) + (nth 1 output) + (if (eq (safe-length output) 3) + 0 + (nth 2 output)) + (car (last output)))))))) (`(:run-program ,file ,_target) (idris-execute-compiled-program file)) (_ nil))) @@ -378,7 +393,7 @@ and semantic annotations PROPS." ,props) (idris-repl-highlight-input start start-line start-col end-line end-col props)))))) - (_ (idris-repl-insert-result result spans)))) ;; The actual result + (_ (idris-repl-insert-result (or result "") spans)))) ;; The actual result ((:error condition &optional spans) (idris-repl-show-abort condition spans)))) @@ -470,7 +485,7 @@ highlighting information from Idris." (defun idris-repl-history-replace (direction) "Replace the current input with the next line in DIRECTION. -DIRECTION is 'forward' or 'backward' (in the history list)." +DIRECTION is `forward' or `backward' (in the history list)." (let* ((min-pos -1) (max-pos (length idris-repl-input-history)) (prefix (idris-repl-history-prefix)) diff --git a/idris-settings.el b/idris-settings.el index 3417667..501f427 100644 --- a/idris-settings.el +++ b/idris-settings.el @@ -342,7 +342,7 @@ using Idris2, then you may wish to customise this variable." (defcustom idris-repl-prompt-style 'short "What sort of prompt to show. -'long shows the Idris REPL prompt, while 'short shows a shorter one." +`long' shows the Idris REPL prompt, while `short' shows a shorter one." :options '(short long) :type 'symbol :group 'idris-repl) diff --git a/test/idris-repl-test.el b/test/idris-repl-test.el index 116f88f..99e218b 100644 --- a/test/idris-repl-test.el +++ b/test/idris-repl-test.el @@ -3,6 +3,10 @@ (require 'ert) (require 'idris-repl) +;; in order to use `idris-quit` +;; TODO: rewrite the test so it is not needed +(require 'idris-commands) + (ert-deftest idris-repl-buffer () ;; Useful while debugging ;; (and (get-buffer idris-repl-buffer-name) (kill-buffer idris-repl-buffer-name)) @@ -46,6 +50,33 @@ (advice-remove 'idris-get-idris-version #'idris-get-idris-version-stub) (setq idris-prompt-string nil)))))) +(ert-deftest idris-repl-event-hook-function () + (let* ((msg "We are about to implicitly bind the following lowercase names.") + (event `(:warning + ("Flycheck.idr" + (4 2) + (4 3) + ,msg + ((186 17 ((:decor :type))) + (205 3 ((:decor :type))) + (235 3 ((:decor :type))) + (262 3 ((:decor :type))) + (268 3 ((:decor :type))) + (302 3 ((:decor :type))) + (328 1 ((:text-formatting :bold) (:decor :postulate))))) + 69)) + (output (cadr event)) + (idris-warnings-printing '(warnings-repl warnings-tree))) + ;; start repl and create connection to Idris + (idris-repl) + (idris-repl-event-hook-function event) + (with-current-buffer "*idris-repl*" + ;; Assert + (let ((str (buffer-substring-no-properties (point-min) (point-max)))) + (should (string-match-p "Flycheck.idr" str)) + (should (string-match-p msg str)))) + (idris-quit))) + ;; https://github.com/idris-hackers/idris-mode/issues/443 (provide 'idris-repl-test) diff --git a/test/idris-xref-test.el b/test/idris-xref-test.el index 7b8bcc4..ce54c3b 100644 --- a/test/idris-xref-test.el +++ b/test/idris-xref-test.el @@ -193,7 +193,8 @@ (with-current-buffer "*xref*" ;; Assert (let ((str (buffer-substring-no-properties (point-min) (point-max)))) - (should (string-match-p "11: AddClause.(-)" str)) + (should (string-match-p "AddClause.(-)" str)) + (should (string-match-p "11:" str)) (should (string-match-p "AddClause.idr" str)) (should (string-match-p "Prelude.Num.(-)" str)) (should (string-match-p "prim__lte_Bits64" str)))