Fix #781 PG does not position to error.

Tests is also added to check the exact position of the error
highlighting.

Description of the fix.

We cannot use the " ^^^ " thing to compute the error location because
commands are not stripped of newlines anymore (#774).

Solution: use the character position information given in the error
message with the following subtleties:

- position are given by coq **bytes** positions.
- position given by coq is the position from the previous "." fed to
  coq. I.e. we must be careful to strip any blank after the final "." of
  a command.
- Coq < 8.11 has a small glitch on positions, the test is compatible
  with both behaviour.
- coq <= 8.20 has a bug on position for curly braces.

In the test we make the disappearing timeout of overlay bigger
so that tests don't fail on slow VMs (maybe useless).

ci/coq-tests.el

@@ -255,12 +255,84 @@ 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))))))
-
+     ;; 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))
+         (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 "reflexivity")))
+                       (equal (span-end sp) (+ 1 proof-cmd-point (length "reflexivity")))))
+           )
+         (should (equal (proof-queue-or-locked-end) proof-point)))))))
+
+
+;; Testing the error location for curly braces specifically. Coq bug
+;; #19355 (coq <= 8.20) needs to be worked around.
+(ert-deftest 51_coq-test-error-highlight ()
+  "Test error highlghting for curly brace."
+  (coq-fixture-on-file
+   (coq-test-full-path "test_error_loc_1.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-lemma*)")
+     ;; 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 "}")
+                                (re-search-backward "}")))) 
+         (message "*** ICI")
+         (coq-test-goto-before " (*test-lemma*)")
+         (proof-goto-point)
+         (proof-shell-wait)
+         (coq-should-buffer-string "Error: The proof is not focused")
+         ;; 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))
+         (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 "}")))
+                       (equal (span-end sp) (+ 1 proof-cmd-point (length "}")))))
+           )
+         (should (equal (proof-queue-or-locked-end) proof-point)))))))
 
 ;; Disable tests that use test_wholefile.v. The file is outdated, uses
 ;; deprecated features, is prone to caues Coq errors and therefore
@@ -376,9 +448,6 @@ For example, COMMENT could be (*test-definition*)"
        (backward-char 3)
        (should (span-at (point) 'proofusing))))))
 
-
-
-
 (provide 'coq-tests)
 
 ;;; coq-tests.el ends here

ci/test_error_loc_1.v

@@ -0,0 +1,9 @@
+Lemma false_proof : forall A B : bool, A = B. 
+Proof.
+  intros A B.
+  destruct A.
+  destruct B.
+  reflexivity. (*error*)
+  }
+Qed. (*test-lemma*)
+

coq/coq.el

@@ -2957,7 +2957,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
   "Last error from `coq-get-last-error-location' and `coq-highlight-error'.")
 
 (defvar coq--error-location-regexp
-  "^Toplevel input[^:]+:\n> \\(.*\\)\n> \\([^^]*\\)\\(\\^+\\)\n"
+  "^Toplevel input, characters \\(?1:[0-9]+\\)-\\(?2:[0-9]+\\):\n"
   "A regexp to search the header of coq error locations.")
 
 ;; I don't use proof-shell-last-output here since it is not always set to the
@@ -2985,43 +2985,27 @@ buffer."
   (if (not parseresp) last-coq-error-location
     ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer
     ;; then highlight the corresponding error location
-    (proof-with-current-buffer-if-exists proof-response-buffer
-      (goto-char (point-max)) ;\nToplevel input, character[^:]:\n
-      (when (re-search-backward coq--error-location-regexp nil t)
-        (let ((text (match-string 1))
-              (pos (length (match-string 2)))
-              (len (length (match-string 3))))
-          ;; clean the response buffer from ultra-ugly underlined command line
-          ;; parsed above. Don't kill the first \n
-          (let ((inhibit-read-only t))
-            (when clean (delete-region (match-beginning 0) (match-end 0))))
-          (when proof-shell-unicode ;; TODO: remove this (when...) when coq-8.3 is out.
-            ;; `pos' and `len' are actually specified in bytes, apparently. So
-            ;; let's convert them, assuming the encoding used is utf-8.
-            ;; Presumably in Emacs-23 we could use `string-bytes' for that
-            ;; since the internal encoding happens to use utf-8 as well.
-            ;; Actually in coq-8.3 one utf8 char = one space so we do not need
-            ;; this at all
-            (let ((bytes text)) ;(encode-coding-string text 'utf-8-unix)
-              ;; Check that pos&len make sense in `bytes', if not give up.
-              (when (>= (length bytes) (+ pos len))
-                ;; We assume here that `text' is a single line and use \n as
-                ;; a marker so we can find it back after decoding.
-                (setq bytes (concat (substring bytes 0 pos)
-                                    "\n" (substring bytes pos (+ pos len))))
-                (let ((chars (decode-coding-string bytes 'utf-8-unix)))
-                  (setq pos (string-match "\n" chars))
-                  (setq len (- (length chars) pos 1))))))
-          (setq last-coq-error-location (list pos len)))))))
-
+    (let* ((reg coq--error-location-regexp)
+           (msg proof-shell-last-response-output))
+      (if (not (string-match reg msg))
+          (setq last-coq-error-location (list 0 0))
+        (let ((pos (string-to-number (match-string 1 msg)))
+              (end (string-to-number (match-string 2 msg))))
+          (setq last-coq-error-location (list pos (- end pos))))))))
+
+(defun point-add-bytes (nbytes)
+  "Return current point shifted by NBYTES bytes."
+  (byte-to-position (+ (position-bytes (point)) nbytes)))
 
 (defun coq-highlight-error (&optional parseresp clean)
-  "Parse the last Coq output looking at an error message.
+  "Return position and length of error in last message.
+
 Highlight the text pointed by it.
 Coq error message must be like this:
 
 \"
-> command with an error here ...
+Toplevel input, characters 60-66:
+> ...
 >                       ^^^^
 \"
 
@@ -3030,20 +3014,35 @@ If PARSERESP is nil, don't really parse response buffer but take the value of
 `last-coq-error-location'.
 
 If PARSERESP and CLEAN are non-nil, delete the error location from the response
-buffer."
+buffer.
+
+Important: Coq gives char positions in bytes instead of chars.
+"
   (proof-with-current-buffer-if-exists proof-script-buffer
     (let ((mtch (coq-get-last-error-location parseresp clean)))
       (when mtch
         (let ((pos (car mtch))
               (lgth (cadr mtch)))
           (goto-char (+ (proof-unprocessed-begin) 1))
           (coq-find-real-start)
-
-          ;; utf8 adaptation is made in coq-get-last-error-location above
-          (let ((time-offset (if coq-time-commands (length coq--time-prefix) 0)))
-            (goto-char (+ (point) pos))
-            (span-make-self-removing-span (point) (+ (point) (- lgth time-offset))
-                                          'face 'proof-warning-face)))))))
+          ;; locations are given in bytes. translate into valid positions
+          ;; + deal with coq bug #19355
+          (let* ((cmdstart (point))
+                 (next-cmd (progn (coq-script-parse-cmdend-forward) (point)))
+                 ;; test suspîcious location info from coq (coq#19355). coq <=
+                 ;; 8.20 on curly braces gives the global location instead of
+                 ;; the location inside the command. fallback: we locate the
+                 ;; error at the command start, with given length. we detect
+                 ;; the problem by testing if the location of the error is
+                 ;; greater than the end of the command itself.
+                 (bug19355 (> pos next-cmd)))
+            (goto-char cmdstart)
+              (let* ((pos (if bug19355 0 pos)) ;; 0 means start of command
+                     (beg (goto-char (point-add-bytes pos)))
+                     (end (goto-char (point-add-bytes lgth))))
+                (span-make-self-removing-span beg end 'face 'proof-warning-face)
+                ;; user usually expect the point to move to the error location
+                (goto-char beg))))))))
 
 (defun coq-highlight-error-hook ()
   (coq-highlight-error t t))

generic/proof-shell.el

@@ -930,6 +930,10 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
 ;;   Low-level commands for shell communication
 ;;
 
+(defun proof-remove-trailing-blanks (s)
+  (let ((pos (string-match "\\s-*\\'" s)))
+    (substring s 0 pos)))
+
 ;;;###autoload
 (defun proof-shell-insert (strings action &optional scriptspan)
   "Insert STRINGS at the end of the proof shell, call `scomint-send-input'.
@@ -969,8 +973,12 @@ used in `proof-add-to-queue' when we start processing a queue, and in
       (run-hooks 'proof-shell-insert-hook)
 
       ;; Replace CRs from string with spaces to avoid spurious prompts.
-      (if proof-shell-strip-crs-from-input
-	  (setq string (subst-char-in-string ?\n ?\  string)))
+      (when proof-shell-strip-crs-from-input
+	(setq string (subst-char-in-string ?\n ?\  string)))
+
+      ;; avoid feeding the proof assistant with blanks at the end that
+      ;; will mess with error locations
+      (setq string (proof-remove-trailing-blanks string))
 
       (insert string)