branch: elpa/proof-general
commit 809b01e845db9dfd3b03a786ca2e2c391a1729de
Merge: e0ec3db200 4cd61e2138
Author: Pierre Courtieu <mata...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #816 from Matafou/fix-first-cmd
Fix problems with error on the first command of a file.
---
ci/coq-tests.el | 42 +++++++++++++++++++++++++++++++++++++++++-
ci/test_error_loc_fst_cmd.v | 4 ++++
coq/coq-indent.el | 3 ++-
3 files changed, 47 insertions(+), 2 deletions(-)
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 78e53dcf93..65bbdd9705 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -446,7 +446,47 @@ For example, COMMENT could be (*test-definition*)"
(coq-test-goto-before "(*proof*)")
(backward-char 3)
(should (span-at (point) 'proofusing))))))
-
+
+
+
+(ert-deftest 110_coq-test-regression_error_on_fst_cmd ()
+ "Test error highlghting in the first line."
+ (coq-fixture-on-file
+ (coq-test-full-path "test_error_loc_fst_cmd.v")
+ (lambda ()
+ (coq-test-goto-before " (*after-error*)")
+ ;; 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-cmd-point (save-excursion
+ (coq-test-goto-before "(*after-error*)")
+ (re-search-backward "bar"))))
+ (coq-test-goto-after " (*after-error*)")
+ (proof-goto-point)
+ (proof-shell-wait)
+ (coq-should-buffer-string "Error: The reference bar was not found in
the current environment.")
+ ;; checking that there is an overlay with warning face
+ ;; exactly on "bar". WARNING: this overlay lasts only for 12
+ ;; secs (thx to the add-timeout above), if this test is done
+ ;; in a (very) slow virtual machine this may fail.
+ (should (equal (point) proof-cmd-point))
+ (let ((sp (span-at proof-cmd-point 'face)))
+ (should sp)
+ (should (equal (span-property sp 'face) 'proof-warning-face))
+ (should (equal (span-start sp) proof-cmd-point))
+ ;; coq-8.11 used to hace ending ps shifted by one
+ (should (or (equal (span-end sp) (+ proof-cmd-point (length "bar")))
+ (equal (span-end sp) (+ 1 proof-cmd-point (length
"bar")))))
+ )
+ (should (equal (proof-queue-or-locked-end) (point-min))))))))
(provide 'coq-tests)
;;; coq-tests.el ends here
diff --git a/ci/test_error_loc_fst_cmd.v b/ci/test_error_loc_fst_cmd.v
new file mode 100644
index 0000000000..72c9541aa1
--- /dev/null
+++ b/ci/test_error_loc_fst_cmd.v
@@ -0,0 +1,4 @@
+Definition foo:= bar. (*after-error*)
+
+Definition foobar := nat.
+
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index b1e3e0425b..7ceff93281 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -208,7 +208,8 @@ position."
(while (coq-looking-at-comment) ;; we are looking for ". " so this is enough
(re-search-backward (concat "\\(?2:"
coq-simple-cmd-ender-prefix-regexp-backward "\\)\\.\\s-") (point-min) 'dummy))
;; unless we reached point-min, jump over the "."
- (when (match-end 2) (goto-char (match-end 2)) (forward-char 1))
+ (when (and (not (eq (point) (point-min))) (match-end 2))
+ (goto-char (match-end 2)) (forward-char 1))
(point))
(defun coq-find-start-of-cmd ()
