Merge pull request #621 from keram/issue-620

Ensure that argument passed to idris-repl-insert-result is a string

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

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)

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))

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)

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)
 

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)))