[nongnu] elpa/proof-general 24da4f5593 3/8: Fix #599, bad detection of "Proof" in "Proof using" suggestions.

[ELPA Syncer]

branch: elpa/proof-general
commit 24da4f559341c651001ef59082006a59ed7a1c41
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

    Fix #599, bad detection of "Proof" in "Proof using" suggestions.
---
 ci/coq-tests.el       | 21 +++++++++++++++++++++
 ci/test_proof_using.v | 12 ++++++++++++
 coq/coq.el            | 49 +++++++++++++++++++++++++++++++++++--------------
 3 files changed, 68 insertions(+), 14 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 3766415545..8d36bab177 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -343,6 +343,27 @@ In nested Ltac calls to \"now (tactic)\" and \"easy\", 
last call failed.
 Tactic failure: Cannot solve this goal."))))
  
 
+(ert-deftest 100_coq-test-proof-using-proof ()
+  "Test for insertion of Proof using annotations"
+  (describe-function 'should)
+  (coq-fixture-on-file
+   (coq-test-full-path "test_proof_using.v")
+   (lambda ()
+     (coq-test-goto-after "(*qed*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (proof-assert-next-command-interactive)
+     (proof-shell-wait)
+     ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show 
Proof."
+     ;(coq-should-buffer-string "\"Proof using\" not set. M-x 
coq-insert-suggested-dependency or right click to add it. See also 
\‘coq-accept-proof-using-suggestion\’.")
+     (save-excursion
+       (coq-test-goto-before "(*proof*)")
+       (backward-char 3)
+       (should (span-at (point) 'proofusing))))))
+ 
+
+
+
 (provide 'coq-tests)
 
 ;;; coq-tests.el ends here
diff --git a/ci/test_proof_using.v b/ci/test_proof_using.v
new file mode 100644
index 0000000000..a4ae3da4e6
--- /dev/null
+++ b/ci/test_proof_using.v
@@ -0,0 +1,12 @@
+
+
+Section S.
+  Variable proof:nat.
+  Hypothesis h: proof = proof.
+  Lemma width_nonneg : proof = proof.
+  Proof. (*proof*)
+    pose proof @h. apply H.
+    (*qed*)
+  Qed.
+  
+End S.
diff --git a/coq/coq.el b/coq/coq.el
index 93cc934fc1..34ea72c0b9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2703,12 +2703,11 @@ insertion point for the \"using\" annotation. ")
 
 ;; span is typically the whole theorem statement+proof span built after a save
 ;; command
-(defun coq-highlight-span-dependencies (span _suggested)
-  (goto-char (span-start span))
+(defun coq-highlight-span-dependencies (start end _suggested)
+  (goto-char start)
   ; Search for the "Proof" command and build a hilighted span on it
-  (let* ((endpos (re-search-forward coq-proof-using-regexp))
-         (proof-pos (match-beginning 0))
-         (newspan (span-make proof-pos endpos)))
+  (let* ((proof-pos (match-beginning 0))
+         (newspan (span-make start end)))
     (span-set-property newspan 'face 'proof-warning-face)
     (span-set-property newspan 'help-echo "Right click to insert \"proof 
using\"")
     (span-set-property newspan 'proofusing t)))
@@ -2727,6 +2726,28 @@ insertion point for the \"using\" annotation. ")
     (coq-insert-proof-using-suggestion span t)
     (span-delete specialspan)))
 
+(defun coq-find-Proof-command (start end)
+  "look for a \"Proof\" command in span SPAN.
+
+Return nil if not found. Set point to the end of \"Proof\"
+otherwise and return position."
+  (goto-char start)
+  (let ((res t) found)
+    (while (and res (null found))
+      (setq res (let ((case-fold-search nil))
+                  (re-search-forward coq-proof-using-regexp end t)))
+      (when res
+        (let ((beg-proof (match-beginning 0))
+              (ins-point (match-beginning 1))
+              (end-cmd (match-end 1)))
+          (if (and res
+                   (save-excursion ;; one more check that it is a Proof command
+                     (goto-char beg-proof)
+                     (equal (point) (coq-find-real-start))))
+              (setq found (list beg-proof ins-point end-cmd))
+            (goto-char end-cmd)))))
+    found))
+
 ;; TODO: have 'ignoe option to completely ignore (not highlight)
 ;; and have 'never renamed into 'highlight
 (defun coq-insert-proof-using-suggestion (span &optional force)
@@ -2736,17 +2757,17 @@ built from the list of strings in SUGGESTED.
 SPAN is the span of the whole theorem (statement + proof)."
   (with-current-buffer proof-script-buffer
     (save-excursion
-      (goto-char (span-start span))
-      (let* ((endpos (re-search-forward coq-proof-using-regexp (span-end span) 
t)))
-        (when endpos
-          (let* ((suggested (span-property span 'dependencies))
-                 (proof-pos (match-beginning 0))
-                 (insert-point (match-beginning 1))
-                 (previous-string (match-string 1))
+      (let ((lproof-info (coq-find-Proof-command (span-start span) (span-end 
span))))
+        (when lproof-info
+          (let* ((proof-pos (car lproof-info)) ;(proof-pos (match-beginning 0))
+                 (insert-point (cadr lproof-info)) ;(insert-point 
(match-beginning 1))
+                 (proof-end (caddr lproof-info))
+                 (previous-string (buffer-substring insert-point proof-end))
                  (previous-content (split-string previous-string))
+                 (suggested (span-property span 'dependencies))
                  (string-suggested (mapconcat #'identity suggested " "))
                  (string-suggested (coq-hack-proofusing-suggestion 
string-suggested))
-                 ;; disabled for now it never happens because Coq would 
suggest anything?
+                 ;; disabled for now it never happens because Coq wouldn't 
suggest anything
                  (same (and nil previous-content
                             (not (cl-set-exclusive-or previous-content 
suggested
                                                       :test 'string-equal))))
@@ -2759,7 +2780,7 @@ SPAN is the span of the whole theorem (statement + 
proof)."
               (if (or force (equal coq-accept-proof-using-suggestion 'always) 
usersayyes)
                   (coq-insert-proof-using proof-pos previous-content 
insert-point string-suggested)
                 (when (member coq-accept-proof-using-suggestion '(highlight 
ask))
-                  (coq-highlight-span-dependencies span string-suggested)
+                  (coq-highlight-span-dependencies proof-pos proof-end 
string-suggested)
                   (message "\"Proof using\" not set. M-x 
coq-insert-suggested-dependency or right click to add it. See also 
`coq-accept-proof-using-suggestion'."))))))))))
 
 (defvar coq-dependencies-system-specific