diff options
author | 2002-07-17 21:21:55 +0000 | |
---|---|---|
committer | 2002-07-17 21:21:55 +0000 | |
commit | 643352f432c596f248b5b876ebf2d06633bddd8b (patch) | |
tree | 30836d6293cc6051f4673ec96fb81ea6a50d2cd2 /generic | |
parent | a6ad5eaddd3637df65cf47523740ba9510be7394 (diff) |
Add note about proof-generic-state-preserving-p
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-script.el | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index c6384550..daffe05d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2439,6 +2439,11 @@ assistant." (defun proof-generic-state-preserving-p (cmd) "Is CMD state preserving? Match on proof-non-undoables-regexp." + ;; FIXME: logic here is not quite finished: proof-non-undoables are + ;; certainly not state preserving, but so are a bunch more things, + ;; i.e. ordinary proof commands which may appear in proof scripts. + ;; Might be better to add positive and negative regexps for + ;; state-preserving tests (only one of which needs to be set). (not (proof-string-match-safe proof-non-undoables-regexp cmd))) (defun proof-generic-count-undos (span) |