Strict read works on GNU Emacs 21.2.

4 files changed, 3 insertions, 27 deletions

diff --git a/BUGS b/BUGS
index d41c366e..47a9b2b1 100644
--- a/BUGS
+++ b/BUGS
@@ -115,21 +115,6 @@ adding this line to .emacs should help:
    (setq process-coding-system-alist '(("" . no-conversion))) 
 
 
-** Strict read only disabled by default in GNU Emacs.
-
-Unfortunately strict read only is incompatible with font lock in
-GNU Emacs, so it is disabled by default.  Instead, you get a warning message
-if the locked region is edited.
-
-
-** In GNU Emacs, spurious "Region read only" errors
-
-Same problem as above, different symptom.
-When proof-strict-read-only is set and font lock is on, these
-errors are given which break font lock.   
-Workaround: turn off proof-strict-read-only, font-lock, or for
-the best of all possible worlds, switch to XEmacs.
-
 
 ** XEmacs undo in the script buffer can edit the "uneditable region"
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index dd72339b..da45d872 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -146,12 +146,7 @@ done if this `proof-strict-state-preserving' is turned off (nil)."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-strict-read-only 
-  ;; For GNU Emacs, strict read only is buggy when used in
-  ;; conjunction with font-lock.
-  ;; The second conjunctive ensures that the expression is either
-  ;; `nil' or `strict' (and not 15!!).  
-  (and proof-running-on-XEmacs 'strict)
+(defcustom proof-strict-read-only 'strict
   "*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
diff --git a/generic/span-extent.el b/generic/span-extent.el
index eda3410d..adf85813 100644
--- a/generic/span-extent.el
+++ b/generic/span-extent.el
@@ -44,9 +44,7 @@
 (defun span-write-warning (span)
   "Give a warning message when SPAN is changed."
   ;; FIXME: implement this in XEmacs, perhaps with after-change-functions
-  ;;
-  (set-span-property span 'read-only nil)
-  )
+  (set-span-property span 'read-only nil))
 
 (defsubst span-property (span name)
   "Return SPAN's value for property PROPERTY."
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index 0abf2cef..d1ff8f6b 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -68,14 +68,12 @@ elements = S0 S1 S2 .... [tl-seq.el]"
 (defun span-read-only-hook (overlay after start end &optional len)
   (error "Region is read-only"))
 
-;;; FIXME: This is too harsh and breaks font-lock
-;;;        If only faces are modified we shouldn't call span-read-only-hook 
 (defun span-read-only (span)
   "Set SPAN to be read only."
   ;; Unfortunately, this function is called on spans which are
   ;; detached from a buffer, which gives an error here, since
   ;; text-properties are associated with text in a particular
-  ;; buffer position.
+  ;; buffer position.  So we use the read only hook instead.
   ;(add-text-properties (span-start span) (span-end span) '(read-only t)))
   (set-span-property span 'modification-hooks '(span-read-only-hook))
   (set-span-property span 'insert-in-front-hooks '(span-read-only-hook)))