From e883e4a33cc15da3db4eb802a4354008fd32fa8a Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 11 Jun 2024 15:36:01 +0200 Subject: [PATCH] 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 68dcf21e3..20a54b6e8 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 03b3f9089..e68bb8f88 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 b48715d55..4d4b5a33e 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))))