Idea for proof-auto-retract, notes about proof-strict-read-only

3 files changed, 20 insertions, 1 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 8bec23e2..15bab2f4 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1649,6 +1649,7 @@ you a reprimand!)
 The default value is @code{strict}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-strict-read-only
 
 @c TEXI DOCSTRING MAGIC: proof-script-indent
 @defopt proof-script-indent 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b46f3d08..ba09379c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -110,7 +110,23 @@ use because of a bug."
   "*Whether Proof General is strict about the read-only region in buffers.
 If non-nil, an error is given when an attempt is made to edit the
 read-only region.  If nil, Proof General is more relaxed (but may give
-you a reprimand!)"
+you a reprimand!)
+
+The default value for proof-strict-read-only depends on which
+version of Emacs you are using.  In FSF Emacs, strict read only is buggy
+when it used in conjunction with font-lock, so it is disabled by default."
+  :type 'boolean
+  :group 'proof-general)
+
+(defcustom proof-auto-retract
+  nil
+  ;; Not implemented yet, only an idea.
+  "*If non-nil, retract automatically when locked region is edited.
+With this option active, the locked region will automatically be
+unlocked when the user attempts to edit it.   To make use of this
+option, proof-strict-read-only should be turned off.
+
+Note: this feature has not been implemented yet."
   :type 'boolean
   :group 'proof-general)
 
diff --git a/todo b/todo
index 0c5eccbc..a50c9f20 100644
--- a/todo
+++ b/todo
@@ -111,6 +111,8 @@ B Check matching code carefully, in view of bug reported (now fixed)
   word matching is based on whitespace constituents or non-word
   constituents.  [6 hrs]
 
+C Implement proof-auto-retract idea.  (4hrs)
+
 C Make and test generic versions of <..>-goal-command-p, 
   <...>-count-undos, to simplify prover-specific code.