[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 1554eb7936 6/8: Merge pull request #648 from
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 1554eb7936 6/8: Merge pull request #648 from Matafou/fix-#599-Proof-using-bad-detection |
Date: |
Tue, 29 Mar 2022 02:58:43 -0400 (EDT) |
branch: elpa/proof-general
commit 1554eb7936f12160d75f3ac2b0336fdfc39fbdc3
Merge: 17a4cc00d6 24da4f5593
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>
Merge pull request #648 from Matafou/fix-#599-Proof-using-bad-detection
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
- [nongnu] elpa/proof-general updated (40c40d229e -> e1e29acb04), ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 3c9bed7061 1/8: Add an option to stop proof-shell-kill-function from killing buffers., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 39911fe049 2/8: Fix #646. Indentation of function arguments., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 1554eb7936 6/8: Merge pull request #648 from Matafou/fix-#599-Proof-using-bad-detection,
ELPA Syncer <=
- [nongnu] elpa/proof-general e1e29acb04 8/8: Merge pull request #639 from Chobbes/save-frames, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 24da4f5593 3/8: Fix #599, bad detection of "Proof" in "Proof using" suggestions., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 17a4cc00d6 5/8: Merge pull request #649 from Matafou/fix-#618-missing-keyword-derive, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general ce033327e3 4/8: Support for command "Derive SuchThat As"., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 0b3454492c 7/8: Merge pull request #647 from Matafou/fix-#646-indent-funargs, ELPA Syncer, 2022/03/29