diff options
| -rw-r--r-- | generic/proof-script.el | 27 | ||||
| -rw-r--r-- | generic/span-extent.el | 1 | ||||
| -rw-r--r-- | generic/span-overlay.el | 2 |
3 files changed, 20 insertions, 10 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 98cd7a35..c2fdba57 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -191,14 +191,20 @@ buffer, so the locked region is made empty by this function." (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." - (proof-span-read-only proof-locked-span)) - +;; These two functions are used in coq.el to edit the locked region +;; (by lifting local (nested) lemmas out of a proof, to make them global). (defsubst proof-unlock-locked () - "Make the locked region read-write." + "Make the locked region writable. +Used in lisp programs for temporary editing of the locked region. +See proof-lock-unlocked for the reverse operation." (span-read-write proof-locked-span)) +(defsubst proof-lock-unlocked () + "Make the locked region read only (according to proof-strict-read-only). +Used in lisp programs for temporary editing of the locked region. +See proof-unlock-locked for the reverse operation." + (proof-span-read-only proof-locked-span)) + (defsubst proof-set-queue-endpoints (start end) "Set the queue span to be START, END." (set-span-endpoints proof-queue-span start end)) @@ -1271,9 +1277,9 @@ the proof script." ;; FIXME da: this could do with some tweaking. Be careful to ;; avoid memory leaks. If a buffer is killed and it's local ;; variables are, then so should all the spans which were allocated -;; for that buffer. Is this what happens? Otherwise we should -;; perhaps *delete* spans corresponding to the locked and -;; queue regions as well as the others. +;; for that buffer. Is this what happens? By garbage collection? +;; Otherwise we should perhaps *delete* spans corresponding to +;; the locked and queue regions as well as the others. (defun proof-restart-buffers (buffers) "Remove all extents in BUFFERS and maybe reset `proof-script-buffer'. No effect on a buffer which is nil or killed. If one of the buffers @@ -1287,7 +1293,10 @@ will deactivated." (if proof-active-buffer-fake-minor-mode (setq proof-active-buffer-fake-minor-mode nil)) (delete-spans (point-min) (point-max) 'type) - (proof-detach-segments buffer))) + (proof-detach-segments buffer) + ;; 29.9.99. Added next line to allow useful toggling + ;; of strict-read-only during a session. + (proof-init-segmentation))) (if (eq buffer proof-script-buffer) (setq proof-script-buffer nil)))) buffers)) diff --git a/generic/span-extent.el b/generic/span-extent.el index 597d262a..a84f91c9 100644 --- a/generic/span-extent.el +++ b/generic/span-extent.el @@ -51,6 +51,7 @@ "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) ) (defsubst span-property (span name) diff --git a/generic/span-overlay.el b/generic/span-overlay.el index 2b969028..7f0bbb34 100644 --- a/generic/span-overlay.el +++ b/generic/span-overlay.el @@ -92,7 +92,7 @@ elements = S0 S1 S2 .... [tl-seq.el]" (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))) + (set-span-property span 'insert-in-front-hooks '(span-give-warning))) (defun int-nil-lt (m n) (cond |