Disable undo in read-only region; add proof-allow-undo-in-read-only setting

3 files changed, 22 insertions, 1 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 5d923d54..77b58077 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2779,6 +2779,7 @@ For multiple frame mode, this function obeys the setting of
 @c Index entries for each option 'concept'
 @cindex User options
 @cindex Strict read-only
+@cindex Undo in read-only region
 @cindex Query program name
 @cindex Dedicated windows
 @cindex Remote host
@@ -2838,7 +2839,7 @@ If you activate this variable, whether or not you really get x-symbol
 support depends on whether your proof assistant supports it and
 whether X-Symbol is installed in your Emacs.
 
-The default value is @code{t}.
+The default value is @code{nil}.
 @end defopt
 
 @c TEXI DOCSTRING MAGIC: proof-output-fontify-enable
@@ -2862,6 +2863,15 @@ you a reprimand!).
 The default value is @code{strict}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-allow-undo-in-read-only
+@defopt proof-allow-undo-in-read-only 
+Whether Proof General allows text undo in the read-only region.@*
+If non-nil, undo will allow altering of processed text (default behaviour
+before Proof General 3.7).  If nil, undo history of processed text is
+discarded.
+
+The default value is @code{nil}.
+@end defopt
 @c TEXI DOCSTRING MAGIC: proof-toolbar-use-button-enablers
 @defopt proof-toolbar-use-button-enablers 
 If non-nil, toolbars buttons may be enabled/disabled automatically.@*
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 22a0f463..feb3c53d 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -197,6 +197,13 @@ you a reprimand!)."
   :set   'proof-set-value
   :group 'proof-user-options)
 
+(defcustom proof-allow-undo-in-read-only nil
+  "*Whether Proof General allows text undo in the read-only region.
+If non-nil, undo will allow altering of processed text (default behaviour
+before Proof General 3.7).  If nil, undo history of processed text is
+discarded."
+  :type  'boolean
+  :group 'proof-user-options)
 
 (defcustom proof-three-window-enable nil
   "*Whether response and goals buffers have dedicated windows.
diff --git a/generic/proof-script.el b/generic/proof-script.el
index eccb7f4b..7ebae6b8 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -204,6 +204,10 @@ scripting buffer may have an active queue span.")
    
 (defsubst proof-set-queue-endpoints (start end)
   "Set the queue span to be START, END."
+  (unless (or (eq buffer-undo-list t) 
+	      proof-allow-undo-in-read-only)
+    (setq buffer-undo-list 
+	  (undo-make-selective-list end (point-max))))
   (span-set-endpoints proof-queue-span start end))
 
 (defsubst proof-set-locked-endpoints (start end)