branch: elpa/proof-general
commit 1226b6b32b11cb22cf639bb7eafa46a73cbc6d59
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
omit-proofs: also omit proofs with bullets and braces
---
ci/simple-tests/coq-test-omit-proofs.el | 1 -
coq/coq-syntax.el | 10 ++++++++++
coq/coq.el | 9 ++++++---
3 files changed, 16 insertions(+), 4 deletions(-)
diff --git a/ci/simple-tests/coq-test-omit-proofs.el
b/ci/simple-tests/coq-test-omit-proofs.el
index 68dcf21e3e..20a54b6e82 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -258,7 +258,6 @@ This test only checks the faces in the middle of the proof."
(should (eq (first-overlay-face) 'proof-omitted-proof-face)))
(ert-deftest omit-proofs-omit-bullets-and-braces ()
- :expected-result :failed
(let ((proof-omit-proofs-option t)
pos-10)
(message "omit-proofs-omit-bullets-and-braces: Check bullets and braces")
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 03b3f9089f..e68bb8f88d 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1433,6 +1433,16 @@ different."
Used in `coq-cmd-prevents-proof-omission' to identify tactics
that only have proof-local effects.")
+(defconst coq-bullet-regexp "^\\(-+\\|\\++\\|\\*+\\)$"
+ "Regular expression matching bullets.
+Used in `coq-cmd-prevents-proof-omission' to identify tactics
+that only have proof-local effects.")
+
+(defconst coq-braces-regexp "^\\({\\|}\\)$"
+ "Regular expression matching braces used for focussing and unfocussing.
+Used in `coq-cmd-prevents-proof-omission' to identify tactics
+that only have proof-local effects.")
+
(defcustom coq-cmd-force-next-proof-kept "Let"
"Instantiating for `proof-script-cmd-force-next-proof-kept'.
Regular expression for commands that prevent omitting the next
diff --git a/coq/coq.el b/coq/coq.el
index b48715d55b..4d4b5a33ec 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -745,9 +745,12 @@ have effects outside the proof, which would prohibit
omitting the
proof, see `proof-script-omit-proofs'.
Commands starting lower case are deemed as tactics that have
-proof local effect only. Everything else is checked against the
-STATECH field in the coq syntax data base, see coq-db.el."
- (if (proof-string-match coq-lowercase-command-regexp cmd)
+proof local effect only and so are bullets and braces. Everything
+else is checked against the STATECH field in the coq syntax data
+base, see coq-db.el."
+ (if (or (proof-string-match coq-lowercase-command-regexp cmd)
+ (proof-string-match coq-bullet-regexp cmd)
+ (proof-string-match coq-braces-regexp cmd))
nil
(not (coq-state-preserving-p cmd))))
