[nongnu] elpa/proof-general 809b01e845 3/3: Merge pull request #816 from Matafou/fix-first-cmd

[ELPA Syncer]

branch: elpa/proof-general
commit 809b01e845db9dfd3b03a786ca2e2c391a1729de
Merge: e0ec3db200 4cd61e2138
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@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 ()