Adding a test for error highlighting.

ci/coq-tests.el

@@ -255,11 +255,24 @@ For example, COMMENT could be (*test-definition*)"
    (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma2*)")
-     (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
-     (proof-goto-point)
-     (proof-shell-wait)
-     (coq-should-buffer-string "Error: Unable to unify \"false\" with \"true\".")
-     (should (equal (proof-queue-or-locked-end) proof-point))))))
+     (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))
+           (proof-cmd-point (save-excursion
+                              (coq-test-goto-after "(*error*)")
+                              (coq-find-real-start)))) 
+       (proof-goto-point)
+       (proof-shell-wait)
+       (coq-should-buffer-string "Error: Unable to unify \"false\" with \"true\".")
+       ;; checking that there is an overlay with warning face exactly
+       ;; on "reflexivity". WARNING: this overlat lasts only for 2
+       ;; secs, if this test is done in a (very) slow virtual machine
+       ;; this may fail.
+       (should (equal (point) proof-cmd-point))
+       (should
+        (let ((sp (span-at (point) 'face)))
+          (and sp (equal (span-property sp 'face) 'proof-warning-face)
+               (equal (span-start sp) (point))
+               (equal (span-end sp) (+ (point) (length "reflexivity"))))))
+       (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
 ;; Disable tests that use test_wholefile.v. The file is outdated, uses

coq/coq.el

@@ -3029,7 +3029,6 @@ Important: Coq gives char positions in bytes instead of chars.
           ;; locations are given in bytes. translate into valid positions
           (let* ((beg (goto-char (point-add-bytes pos)))
                  (end (goto-char (point-add-bytes lgth))))
-            (message "*** beg = %S/%S, end = %S/%S" pos beg lgth end)
             (goto-char beg) ;; move point to error
             (span-make-self-removing-span beg end 'face 'proof-warning-face)))))))