diff options
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 11 |
1 files changed, 7 insertions, 4 deletions
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, |