From 6f4a3a07fcc4604fa99991d60762a446ac7e4fd3 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 2 Sep 2024 18:18:45 +0200 Subject: [PATCH] Adding a bigger timeout to errro overlays. --- ci/coq-tests.el | 50 ++++++++++++++++++++++++++++++------------------- coq/coq.el | 14 +++++++++++--- 2 files changed, 42 insertions(+), 22 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index d4c9784f7..193bab0ea 100644 --- 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 index 65457023f..a6a4336c0 100644 --- 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))