diff options
| -rw-r--r-- | doc/PG-adapting.texi | 15 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 4 | ||||
| -rw-r--r-- | generic/proof-config.el | 11 | ||||
| -rw-r--r-- | generic/proof-script.el | 62 |
4 files changed, 62 insertions, 30 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 3b9ebb2a..74d576c1 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1162,7 +1162,9 @@ expressions to search for commands that start found, the opaque proof is replaced with a cheating command (@code{proof-script-proof-admit-command}). From this description it is immediate, that the omit proof feature does only work if -proofs are not nested. +proofs are not nested. If a nested proof is found, a warning is +displayed and omitting proofs stops at that location for the +currently asserted region. To enable the omit proofs feature, the following settings must be configured. @@ -1192,10 +1194,13 @@ the match of @samp{@code{proof-script-definition-end-regexp}}) is considered to be not opaque and not omitted, thus all these proof commands _are_ sent to the proof assistant. -If a match for @samp{@code{proof-script-proof-start-regexp}} is found before -the next match for @samp{@code{proof-script-proof-end-regexp}} or -@samp{@code{proof-script-definition-end-regexp}}, an error is signaled to the -user. +The feature does not work for nested proofs. If a match for +@samp{@code{proof-script-proof-start-regexp}} is found before the next match +for @samp{@code{proof-script-proof-end-regexp}} or +@samp{@code{proof-script-definition-end-regexp}}, the search for opaque +proofs immediately stops and all commands following the previous +match of @samp{@code{proof-script-proof-start-regexp}} are sent verbatim to +the proof assistant. All the regular expressions for this feature are matched against the commands inside proof action items, that is as strings, diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index c8f0c4c7..43f3ccb0 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -5221,6 +5221,10 @@ With a prefix argument, both @code{proof-goto-point} and @code{proof-process-buffer} will temporarily disable the omit proofs feature and send the full proof script to Coq. +If a nested proof is detected while searching for opaque proofs +to omit, a warning is displayed and the complete remainder of the +asserted region is sent unmodified to Coq. + @node Editing multiple proofs @section Editing multiple proofs diff --git a/generic/proof-config.el b/generic/proof-config.el index 011a6625..951aade2 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -720,10 +720,13 @@ the match of `proof-script-definition-end-regexp') is considered to be not opaque and not omitted, thus all these proof commands _are_ sent to the proof assistant. -If a match for `proof-script-proof-start-regexp' is found before -the next match for `proof-script-proof-end-regexp' or -`proof-script-definition-end-regexp', an error is signaled to the -user. +The feature does not work for nested proofs. If a match for +`proof-script-proof-start-regexp' is found before the next match +for `proof-script-proof-end-regexp' or +`proof-script-definition-end-regexp', the search for opaque +proofs immediately stops and all commands following the previous +match of `proof-script-proof-start-regexp' are sent verbatim to +the proof assistant. All the regular expressions for this feature are matched against the commands inside proof action items, that is as strings, diff --git a/generic/proof-script.el b/generic/proof-script.el index e9adc199..0c4a980d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2022,14 +2022,33 @@ start is found inside a proof." nil "proof-script omit proof feature not properly configured") (let (result maybe-result inside-proof - proof-start-span-start proof-start-span-end) - (dolist (item vanillas (nreverse (nconc maybe-result result))) - (let ((cmd (mapconcat 'identity (nth 1 item) " "))) - (if inside-proof - (progn - (when (string-match proof-script-proof-start-regexp cmd) + proof-start-span-start proof-start-span-end + 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 - (error "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) + (setq vanillas nil) + ;; for Coq nobody will notice the warning, because + ;; the error about nested proofs will pop up shortly + ;; afterwards + (display-warning + '(proof-script) + ;; use the end of the span, because the start is + ;; usually on the preceding line + (format (concat "found second proof start at line %d" + " - are there nested proofs?") + (line-number-at-pos (span-end (car item)))))) (if (string-match proof-script-proof-end-regexp cmd) (let ;; Reuse the Qed span for the whole proof, @@ -2078,20 +2097,21 @@ start is found inside a proof." (setq inside-proof nil)) ;; normal proof command - maybe it belongs to a ;; Defined, keep it separate, until we know. - (push item maybe-result)))) - ;; outside proof - (if (string-match proof-script-proof-start-regexp cmd) - (progn - (setq maybe-result nil) - ;; Keep the Proof using command in any case. - (push item result) - (setq proof-start-span-start (span-start (car item))) - (setq proof-start-span-end (span-end (car item))) - (setq inside-proof t)) - ;; outside, no proof start - keep it unmodified - (push item result))))) - ;; return (nreverse (nconc maybe-result result)), see dolist above - )) + (push item maybe-result))))) + ;; outside proof + (if (string-match proof-script-proof-start-regexp cmd) + (progn + (setq maybe-result nil) + ;; Keep the Proof using command in any case. + (push item result) + (setq proof-start-span-start (span-start (car item))) + (setq proof-start-span-end (span-end (car item))) + (setq inside-proof t)) + ;; outside, no proof start - keep it unmodified + (push item result))) + (setq vanillas (cdr vanillas))) + (nreverse (nconc maybe-result result)))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |