Added proof-strict-read-only, probably a handy new user-option.

Side effect is that it's default value of nil for FSF Emacs avoids the
font lock problem with span-read-only for FSF Emacs.
XEmacs does not have the warning message implemented yet.

4 files changed, 58 insertions, 3 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4ed17b58..b7860a3f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -96,6 +96,17 @@ for experienced Emacs users."
   :type 'boolean
   :group 'proof-general)
 
+(defcustom proof-strict-read-only 
+  ;; For FSF Emacs, strict read only is buggy when used in
+  ;; conjunction with font-lock.
+  (string-match "XEmacs" emacs-version)
+  "*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!)"
+  :type 'boolean
+  :group 'proof-general)
+
 ;;
 ;; Faces.
 ;; We ought to test that these work sensibly:
diff --git a/generic/proof-script.el b/generic/proof-script.el
index aa59381c..f9b4a0b4 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -95,9 +95,27 @@ This function coincides with `append-element' in the package
 ;; proof-init-segmentation, which can happen when a file is visited.
 ;; So nasty things might happen if a locked file is visited whilst
 ;; another buffer has a non-empty queue region being processed.
+
+
 (deflocal proof-queue-span nil
   "The queue span of the buffer.")
 
+;; FIXME da: really the queue region should always be locked strictly.
+
+(defun proof-span-read-only (span)
+  "Make span be read-only, if proof-strict-read-only is non-nil.
+Otherwise make span give a warning message on edits."
+  (if proof-strict-read-only
+      (span-read-only span)
+    (span-write-warning span)))
+
+;; not implemented yet
+;; (defun proof-toggle-strict-read-only ()
+;;  "Toggle proof-strict-read-only, changing current spans."
+;;  (interactive)
+;;   map-spans blah
+;;  )
+
 (defun proof-init-segmentation ()
   "Initialise the spans in a proof script buffer."
   ;; Initialise queue span, remove it from buffer.
@@ -105,7 +123,7 @@ This function coincides with `append-element' in the package
       (setq proof-queue-span (make-span 1 1)))
   (set-span-property proof-queue-span 'start-closed t)
   (set-span-property proof-queue-span 'end-open t)
-  (span-read-only proof-queue-span)
+  (proof-span-read-only proof-queue-span)
   (set-span-property proof-queue-span 'face 'proof-queue-face)
   (detach-span proof-queue-span)
   ;;
@@ -117,13 +135,13 @@ This function coincides with `append-element' in the package
       (setq proof-locked-span (make-span 1 1)))
   (set-span-property proof-locked-span 'start-closed t)
   (set-span-property proof-locked-span 'end-open t)
-  (span-read-only proof-locked-span)
+  (proof-span-read-only proof-locked-span)
   (set-span-property proof-locked-span 'face 'proof-locked-face)
   (detach-span proof-locked-span))
 
 (defsubst proof-lock-unlocked ()
   "Make the locked region read only."
-  (span-read-only proof-locked-span))
+  (proof-span-read-only proof-locked-span))
 
 (defsubst proof-unlock-locked ()
   "Make the locked region read-write."
diff --git a/generic/span-extent.el b/generic/span-extent.el
index db1a70cd..fcc82258 100644
--- a/generic/span-extent.el
+++ b/generic/span-extent.el
@@ -43,6 +43,16 @@
   "Set SPAN to be writeable."
   (set-span-property span 'read-only nil))
 
+(defun span-give-warning ()
+  "Give a warning message."
+  (message "You should not edit here!"))
+
+(defun span-write-warning (span)
+  "Give a warning message when SPAN is changed."
+  ;; FIXME: implement this in XEmacs, perhaps with after-change-functions
+  ;;
+  )
+
 (defsubst span-property (span name)
   "Return SPAN's value for property PROPERTY."
   (extent-property span name))
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index 6d8b270e..fa113911 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -63,19 +63,35 @@ elements = S0 S1 S2 .... [tl-seq.el]"
   "Return SPAN's value for property PROPERTY."
   (overlay-get span name))
 
+;; This function is problematical with font-lock turned on.
 (defun span-read-only-hook (overlay after start end &optional len)
   (error "Region is read-only"))
 
 (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 her, since
+  ;; text-properties are associated with text in a particular
+  ;; buffer position.
+  ;(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)))
 
 (defun span-read-write (span)
   "Set SPAN to be writeable."
+  ;; See comment above for text properties problem.
   (set-span-property span 'modification-hooks nil)
   (set-span-property span 'insert-in-front-hooks nil))
 
+(defun span-give-warning (&rest args)
+  "Give a warning message."
+  (message "You should not edit here!"))
+
+(defun span-write-warning (span)
+  "Give a warning message when SPAN is changed."
+  (set-span-property span 'modification-hooks '(span-give-warning))
+  (set-span-property span 'modification-hooks '(span-give-warning)))
+
 (defun int-nil-lt (m n)
   (cond
    ((eq m n) nil)