Adding a bigger timeout to errro overlays.

Matafou · Sep 2, 2024 · 6f4a3a0 · 6f4a3a0
1 parent a86edc9
commit 6f4a3a0
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 22 deletions.
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
@@ -255,25 +255,37 @@ 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-cmd-point (save-excursion
-                              (coq-test-goto-after "(*error*)")
-                              (re-search-forward "reflexivity")
-                              (re-search-backward "reflexivity")))) 
-       (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))))))
+     ;; redefining this function locally so that self removing spans
+     ;; remain longer. Cf span.el
+     (cl-letf (((symbol-function 'span-make-self-removing-span)
+                (lambda (beg end &rest props)
+                  (let ((ol (span-make beg end)))
+                    (while props
+                      (overlay-put ol (car props) (cadr props))
+                      (setq props (cddr props)))
+                    (add-timeout 10 'delete-overlay ol)
+                    ol))))
+
+       (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)") (point)))
+             (proof-cmd-point (save-excursion
+                                (coq-test-goto-after "(*error*)")
+                                (re-search-forward "reflexivity")
+                                (re-search-backward "reflexivity")))) 
+         (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 proof-cmd-point 'face)))
+            (and sp (equal (span-property sp 'face) 'proof-warning-face)
+                 (equal (span-start sp) proof-cmd-point)
+                 (equal (span-end sp) (+ proof-cmd-point (length "reflexivity")))
+                 )))
+         (should (equal (proof-queue-or-locked-end) proof-point)))))))
 
 
 ;; Disable tests that use test_wholefile.v. The file is outdated, uses

diff --git a/coq/coq.el b/coq/coq.el
@@ -3026,10 +3026,18 @@ Important: Coq gives char positions in bytes instead of chars.
           (goto-char (+ (proof-unprocessed-begin) 1))
           (coq-find-real-start)
           ;; locations are given in bytes. translate into valid positions
-          (let* ((beg (goto-char (point-add-bytes pos)))
+          (let* ((cmdstart (point))
+                 (len (- (save-excursion (coq-script-parse-cmdend-forward) (point)) (point)))
+                 (beg (goto-char (point-add-bytes pos)))
                  (end (goto-char (point-add-bytes lgth))))
-            (goto-char beg) ;; move point to error
-            (span-make-self-removing-span beg end 'face 'proof-warning-face)))))))
+            (if (not (and (<= pos len) (<= end (+ beg len))))
+                ;; positions seem wrong (e.g. coq bug #19355), fallback:
+                (progn
+                  (goto-char cmdstart)
+                  (span-make-self-removing-span cmdstart (+ cmdstart len 2) 'face 'proof-warning-face))
+              (goto-char beg) ;; move point to error
+              (span-make-self-removing-span beg end 'face 'proof-warning-face)
+)))))))
 
 (defun coq-highlight-error-hook ()
   (coq-highlight-error t t))