[nongnu] elpa/proof-general 067bffa4bb 07/10: Merge pull request #782 from Matafou/fix-no-strip-newlines

[ELPA Syncer]

branch: elpa/proof-general
commit 067bffa4bb0f11f163a7c47b4cb562e37b1fbe46
Merge: c3e6c391e7 037baeafcb
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #782 from Matafou/fix-no-strip-newlines
    
    Fix #781 PG does not position to error + other buggy locations.
---
 ci/coq-tests.el       |  86 ++++++++++++++++++++++++++---
 ci/test_error_loc_1.v |   9 +++
 coq/coq.el            | 150 ++++++++++++++++++++++++++------------------------
 3 files changed, 164 insertions(+), 81 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 9b2a96d661..78e53dcf93 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -255,12 +255,83 @@ 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 "}")))) 
+         (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 +447,6 @@ For example, COMMENT could be (*test-definition*)"
        (backward-char 3)
        (should (span-at (point) 'proofusing))))))
  
-
-
-
 (provide 'coq-tests)
 
 ;;; coq-tests.el ends here
diff --git a/ci/test_error_loc_1.v b/ci/test_error_loc_1.v
new file mode 100644
index 0000000000..89ddd4b424
--- /dev/null
+++ b/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*)
+  
diff --git a/coq/coq.el b/coq/coq.el
index 9d23dafca0..4eb4938106 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -121,8 +121,8 @@ Namely, goals that do not fit in the goals window."
      ;; Should this variable be buffer-local? No opinion on that but if yes we
      ;; should re-intialize to coq-search-blacklist-string instead of
      ;; keeping the current value (that may come from another file).
-     ,(format "Add Search Blacklist %s. " coq-search-blacklist-current-string))
-   '("Set Suggest Proof Using. ") coq-user-init-cmd)
+     ,(format "Add Search Blacklist %s." coq-search-blacklist-current-string))
+   '("Set Suggest Proof Using.") coq-user-init-cmd)
   "Command to initialize the Coq Proof Assistant.")
 
 ;; FIXME: Even if we don't use coq-indent for indentation, we still need it for
@@ -338,10 +338,6 @@ It is mostly useful in three window mode, see also
     (filtered-frame-list (lambda (x) (and (member x frame-resp) (member x 
frame-gls))))))
 
 
-(defun coq-remove-trailing-blanks (s)
-  (let ((pos (string-match "\\s-*\\'" s)))
-    (substring s 0 pos)))
-
 (defun coq-remove-starting-blanks (s)
   (string-match "\\`\\s-*" s)
   (substring s (match-end 0) (length s)))
@@ -454,7 +450,7 @@ This is a subroutine of `proof-shell-filter'."
          ;;         'proof-eager-annotation-face))
          (str (proof-shell-strip-eager-annotations start end))
          (strnotrailingspace
-          (coq-remove-starting-blanks (coq-remove-trailing-blanks str))))
+          (coq-remove-starting-blanks (proof-strip-whitespace-at-end str))))
     (pg-response-display-with-face strnotrailingspace))) ; face
 
 
@@ -708,7 +704,7 @@ If locked span already has a state number, then do nothing. 
Also updates
       (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer))
       (setq coq--retract-naborts naborts)
       (list
-       (format "BackTo %s . "
+       (format "BackTo %s ."
                (int-to-string span-staten))))))
 
 (defvar coq-current-goal 1
@@ -901,7 +897,7 @@ is nil (t by default)."
                       (if shft (if id "About" "Locate")
                         (if ctrl (if id "Print" "Locate")))))))
         (proof-shell-invisible-command
-         (format (concat  cmd " %s . ")
+         (format (concat  cmd " %s .")
                  ;; Notation need to be surrounded by ""
                  (if id id (concat "\"" notat "\""))))))))
 
@@ -929,7 +925,7 @@ Otherwise propose identifier at point if any."
     (proof-shell-ready-prover)
     (setq cmd (coq-guess-or-ask-for-string ask dontguess))
     (proof-shell-invisible-command
-     (format (concat do " %s . ") (funcall postform cmd))
+     (format (concat do " %s .") (funcall postform cmd))
      wait)))
 
 
@@ -950,12 +946,12 @@ the time of writing this documentation)."
     ;; to trigger "Show" or anything that we usually insert after a group of
     ;; commands.
     (unless flag-is-on (proof-shell-invisible-command
-                        (format " %s . " (funcall postform setcmd))
+                        (format " %s ." (funcall postform setcmd))
                         nil nil 'no-response-display 'empty-action-list))
     (proof-shell-invisible-command
-     (format " %s . " (funcall postform cmd)) 'wait nil 'empty-action-list)
+     (format " %s ." (funcall postform cmd)) 'wait nil 'empty-action-list)
     (unless flag-is-on (proof-shell-invisible-command
-                        (format " %s . " (funcall postform unsetcmd))
+                        (format " %s ." (funcall postform unsetcmd))
                         'waitforit  nil 'no-response-display 
'empty-action-list))))
 
 (defun coq-ask-do-set-unset (ask do setcmd unsetcmd
@@ -995,7 +991,7 @@ UNSETCMD.  See `coq-command-with-set-unset'."
   ;;   (setq cmd (coq-guess-or-ask-for-string ask dontguess))
   ;;   (coq-command-with-set-unset
   ;;    "Set Printing Implicit"
-  ;;    (format (concat do " %s . ") cmd)
+  ;;    (format (concat do " %s .") cmd)
   ;;    "Unset Printing Implicit" )
   ;;   ))
 
@@ -1090,7 +1086,7 @@ This is specific to `coq-mode'."
    ))
 
 (defun coq-set-undo-limit (undos)
-  (proof-shell-invisible-command (format "Set Undo %s . " undos)))
+  (proof-shell-invisible-command (format "Set Undo %s ." undos)))
 
 (defun coq-Pwd ()
   "Display the current Coq working directory."
@@ -1764,7 +1760,7 @@ See  `coq-fold-hyp'."
     (coq-fold-hyp h)))
 ;;;;;;;
 
-(proof-definvisible coq-PrintHint "Print Hint. ")
+(proof-definvisible coq-PrintHint "Print Hint.")
 
 ;; Items on show menu
 (proof-definvisible coq-show-tree "Show Tree.")
@@ -1788,8 +1784,8 @@ See  `coq-fold-hyp'."
 (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.")
 (proof-definvisible coq-unset-printing-wildcards "Unset Printing Wildcard.")
 ; Takes an argument
-;(proof-definvisible coq-set-printing-printing-depth "Set Printing Printing 
Depth . ")
-;(proof-definvisible coq-unset-printing-printing-depth "Unset Printing 
Printing Depth . ")
+;(proof-definvisible coq-set-printing-printing-depth "Set Printing Printing 
Depth .")
+;(proof-definvisible coq-unset-printing-printing-depth "Unset Printing 
Printing Depth .")
 
 ;; Persistent setting, non-boolean, non cross-version compatible (Coq >= 8.10)
 (defconst coq-diffs--function #'coq-diffs
@@ -1907,11 +1903,11 @@ at `proof-assistant-settings-cmds' evaluation time.")
   (setq proof-query-file-save-when-activating-scripting nil)
 
   ;; Commands sent to proof engine
-  (setq proof-showproof-command "Show. "
-        proof-context-command "Print All. "
-        proof-goal-command "Goal %s. "
-        proof-save-command "Save %s. "
-        proof-find-theorems-command "Search %s. ")
+  (setq proof-showproof-command "Show."
+        proof-context-command "Print All."
+        proof-goal-command "Goal %s."
+        proof-save-command "Save %s."
+        proof-find-theorems-command "Search %s.")
 
   (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp)
 
@@ -1946,8 +1942,8 @@ at `proof-assistant-settings-cmds' evaluation time.")
   ;; span menu
   (setq proof-script-span-context-menu-extensions #'coq-create-span-menu)
 
-  (setq proof-shell-start-silent-cmd "Set Silent. "
-        proof-shell-stop-silent-cmd "Unset Silent. ")
+  (setq proof-shell-start-silent-cmd "Set Silent."
+        proof-shell-stop-silent-cmd "Unset Silent.")
 
   ;; prooftree config
   (setq
@@ -2074,7 +2070,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
 
 
 (defun coq-goals-mode-config ()
-  (setq pg-goals-change-goal "Show %s . ")
+  (setq pg-goals-change-goal "Show %s .")
   (setq pg-goals-error-regexp coq-error-regexp)
   (setq proof-goals-font-lock-keywords coq-goals-font-lock-keywords)
   (proof-goals-config-done))
@@ -2097,7 +2093,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
 ;; (defpacustom print-only-first-subgoal  nil
 ;;  "Whether to just print the first subgoal in Coq."
 ;;  :type 'boolean
-;;  :setting ("Focus. " . "Unfocus. "))
+;;  :setting ("Focus." . "Unfocus."))
 
 
 (defpacustom hide-additional-subgoals nil
@@ -2118,20 +2114,20 @@ at `proof-assistant-settings-cmds' evaluation time.")
 ;(defpacustom print-fully-explicit nil
 ;  "Print fully explicit terms."
 ;  :type 'boolean
-;  :setting ("Set Printing All. " . "Unset Printing All. "))
+;  :setting ("Set Printing All." . "Unset Printing All."))
 ;
 
 (defpacustom printing-depth 50
   "Depth of pretty printer formatting, beyond which dots are displayed."
   :type 'integer
-  :setting "Set Printing Depth %i . ")
+  :setting "Set Printing Depth %i .")
 
 (defun coq-diffs ()
   "Return string for setting Coq Diffs.
 Return the empty string if the version of Coq < 8.10."
   (setq pg-insert-text-function #'coq-insert-tagged-text)
   (if (coq--post-v810)
-      (format "Set Diffs \"%s\". " (symbol-name coq-diffs))
+      (format "Set Diffs \"%s\"." (symbol-name coq-diffs))
     ""))
 
 (defun coq-diffs--setter (symbol new-value)
@@ -2159,7 +2155,7 @@ Set Diffs setting if Coq is running and has a version >= 
8.10."
 ;;(defpacustom undo-depth coq-default-undo-limit
 ;;  "Depth of undo history.  Undo behaviour will break beyond this size."
 ;;  :type 'integer
-;;  :setting "Set Undo %i . ")
+;;  :setting "Set Undo %i .")
 
 ;; Problem if the Remove or Add fails we leave Coq's blacklist in a strange
 ;; state: unnoticed by the user, and desynched from
@@ -2327,7 +2323,10 @@ Return command that undos to state."
       ;; Don't add the prefix if this is a command sent internally
       (unless (or (eq action 'proof-done-invisible)
                   (coq-bullet-p string)) ;; coq does not accept "Time -".
-        (setq string (concat coq--time-prefix string))))))
+        (setq string (concat coq--time-prefix string))
+        ;; coqtop *really wants* a newline after a comand-ending dot.
+        ;; (error) locations are very wrong otherwise
+        (setq string (proof-strip-whitespace-at-end string))))))
 
 (add-hook 'proof-shell-insert-hook #'coq-preprocessing)
 
@@ -2957,7 +2956,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> 
[^\n]*\\)*\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
@@ -2966,12 +2965,16 @@ Completion is on a quasi-exhaustive list of Coq 
tacticals."
 ;; buffer (better to only scroll it?)
 (defun coq-get-last-error-location (&optional parseresp clean)
   "Return location information on last error sent by coq.
+
 Return a two elements list (POS LEN) if successful, nil otherwise.
-POS is the number of characters preceding the underlined expression,
-and LEN is its length.
-Coq error message must be like this:
+
+POS is the number of **bytes** preceding the error location in
+the current command, and LEN is its length (in bytes too).
+
+Coq error message is like this:
 
 \"
+Toplevel input, characters 22-26:
 > command with an error here ...
 >                       ^^^^
 \"
@@ -2983,45 +2986,33 @@ If PARSERESP is nil, don't really parse response buffer 
but take the value of
 If PARSERESP and CLEAN are non-nil, delete the error location from the response
 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))))
+      (goto-char (point-max))
+      (if (not (re-search-backward coq--error-location-regexp nil t))
+          (setq last-coq-error-location (list 0 0))
+        (let ((pos (string-to-number (match-string 1)))
+              (end (string-to-number (match-string 2))))
+          (setq last-coq-error-location (list pos (- end pos)))
           ;; clean the response buffer from ultra-ugly underlined command line
-          ;; parsed above. Don't kill the first \n
+          ;; Don't kill the first \n
+          ;; TODO: make coq stop displaying it it?
           (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)))))))
+            (when clean (delete-region (match-beginning 0) (match-end 0)))))
+        last-coq-error-location))))
 
+(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,7 +3021,10 @@ 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
@@ -3038,12 +3032,24 @@ buffer."
               (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))