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

2 files changed, 11 insertions, 0 deletions

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)