[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 4a4a5cc8f4 1/2: proof-script, test-omit-proo
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 4a4a5cc8f4 1/2: proof-script, test-omit-proofs: style and documentation improvements |
Date: |
Fri, 17 Mar 2023 17:02:13 -0400 (EDT) |
branch: elpa/proof-general
commit 4a4a5cc8f4be16c1748ac81f0213ee981ffc42f9
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
proof-script,test-omit-proofs: style and documentation improvements
---
ci/simple-tests/test-omit-proofs.el | 4 ++--
generic/proof-script.el | 30 +++++++++++++++++++++++-------
2 files changed, 25 insertions(+), 9 deletions(-)
diff --git a/ci/simple-tests/test-omit-proofs.el
b/ci/simple-tests/test-omit-proofs.el
index 64dcb6473b..edc8491b9c 100644
--- a/ci/simple-tests/test-omit-proofs.el
+++ b/ci/simple-tests/test-omit-proofs.el
@@ -13,7 +13,7 @@
;;
;; Test that with proof-omit-proofs-option
;; - the proof _is_ processed when using a prefix argument
-;; - in this case the proof as normal locked color
+;; - in this case the proof has normal locked color
;; - without prefix arg, the proof is omitted
;; - the proof has omitted color then
;; - stuff before the proof still has normal color
@@ -52,7 +52,7 @@ therefore have a higher priority."
(defun overlays-at-point-sorted ()
"Return overlays at point in decreasing order of priority.
-Works only if no overlays has a priority property. Same
+Works only if no overlay has a priority property. Same
'(overlays-at (point) t)', except that it also works on Emacs <= 25."
(sort (overlays-at (point) t) 'overlay-less))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 31e5d083b2..be884c1158 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2022,23 +2022,32 @@ start is found inside a proof."
proof-script-proof-admit-command)
nil
"proof-script omit proof feature not properly configured")
- (let (result maybe-result inside-proof
+ (let (;; result vanillas with omitted proofs in reverse order
+ result
+ ;; commands of current proof before deciding opaqueness in reverse
order
+ maybe-result
+ inside-proof
proof-start-span-start proof-start-span-end
- item cmd)
+ ;; the current vanilla item
+ item
+ ;; the command of the current item
+ cmd)
(while vanillas
(setq item (car vanillas))
;; cdr vanillas is at the end of the loop
(setq cmd (mapconcat #'identity (nth 1 item) " "))
+
(if inside-proof
(progn
(if (string-match proof-script-proof-start-regexp cmd)
- ;; found another proof start inside a proof
- ;; stop omitting and pass the remainder unmodified
- ;; the result in `result' is aggregated in reverse
- ;; order, need to reverse vanillas
+ ;; Found another proof start inside a proof.
+ ;; Stop omitting and pass the remainder unmodified.
+ ;; The result in `result' is aggregated in reverse
+ ;; order, need to reverse vanillas.
(progn
(setq result (nconc (nreverse vanillas) maybe-result result))
(setq maybe-result nil)
+ ;; terminate the while loop
(setq vanillas nil)
;; for Coq nobody will notice the warning, because
;; the error about nested proofs will pop up shortly
@@ -2050,6 +2059,8 @@ start is found inside a proof."
(format (concat "found second proof start at line %d"
" - are there nested proofs?")
(line-number-at-pos (span-end (car item))))))
+
+ ;; else - no nested proof, but still inside-proof
(if (string-match proof-script-proof-end-regexp cmd)
(let
;; Reuse the Qed span for the whole proof,
@@ -2089,6 +2100,8 @@ start is found inside a proof."
'proof-done-advancing nil)
result)
(setq inside-proof nil))
+
+ ;; else - no nested proof, no opaque proof, but still inside
(if (string-match proof-script-definition-end-regexp cmd)
;; A proof ending in Defined or something similar.
;; Need to keep all commands from the start of the proof.
@@ -2099,7 +2112,8 @@ start is found inside a proof."
;; normal proof command - maybe it belongs to a
;; Defined, keep it separate, until we know.
(push item maybe-result)))))
- ;; outside proof
+
+ ;; else - outside proof
(if (string-match proof-script-proof-start-regexp cmd)
(progn
(setq maybe-result nil)
@@ -2111,6 +2125,8 @@ start is found inside a proof."
;; outside, no proof start - keep it unmodified
(push item result)))
(setq vanillas (cdr vanillas)))
+
+ ;; end of loop - return filtered vanillas
(nreverse (nconc maybe-result result))))