From 643352f432c596f248b5b876ebf2d06633bddd8b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 17 Jul 2002 21:21:55 +0000
Subject: Add note about proof-generic-state-preserving-p

---
 generic/proof-script.el | 5 +++++
 1 file changed, 5 insertions(+)

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)
-- 
cgit v1.2.3