Add proof-colour-locked option to leave locked region background uncoloured.

3 files changed, 21 insertions, 2 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 87b36e2f..bac0c84a 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -245,6 +245,13 @@ Proof General."
   :type 'boolean
   :group 'proof-user-options)
 
+(defcustom proof-colour-locked t
+  "*If non-nil, colour the locked region with `proof-locked-face'.
+If this is not set, buffers will have no special face set
+on locked regions."
+  :type 'boolean
+  :set 'proof-set-value
+  :group 'proof-user-options)
 
 (defcustom proof-query-file-save-when-activating-scripting
   t
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 55c8e5a7..b0e774e6 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -264,6 +264,7 @@ without adjusting window layout."
 (proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle)
 (proof-deftoggle proof-disappearing-proofs)
 (proof-deftoggle proof-strict-read-only)
+(proof-deftoggle proof-colour-locked)
 
 (proof-deftoggle-fn 'proof-imenu-enable 'proof-imenu-toggle)
 (proof-deftoggle proof-keep-response-history)
@@ -391,7 +392,11 @@ without adjusting window layout."
        :active (not proof-multiple-frames-enable)
        :style toggle
        :selected proof-shrink-windows-tofit
-       :help "Dynamically shrink size of output panes to fit contents"])
+       :help "Dynamically shrink size of output panes to fit contents"]
+      ["Colour locked" proof-colour-locked
+       :style toggle
+       :selected proof-colour-locked
+       :help "Use decoration of locked region"])
      ("Follow Mode" 
       ["Follow Locked Region" 
        (customize-set-variable 'proof-follow-mode 'locked)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 1f554f39..cc437eb5 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -294,13 +294,20 @@ Also clear list of script portions."
   (span-set-property proof-locked-span 'start-closed t)
   (span-set-property proof-locked-span 'end-open t)
   (proof-span-read-only proof-locked-span)
-  (span-set-property proof-locked-span 'face 'proof-locked-face)
+  (if proof-colour-locked
+      (span-set-property proof-locked-span 'face 'proof-locked-face))
   (span-detach proof-locked-span)
   (setq proof-last-theorem-dependencies nil)
   (setq proof-element-counters nil)
   (pg-clear-script-portions)
   (pg-clear-input-ring))
 
+;;;###autoload
+(defun proof-colour-locked ()
+  (interactive)
+  (if proof-colour-locked
+      (span-set-property proof-locked-span 'face 'proof-locked-face)
+    (span-set-property  proof-locked-span 'face nil)))
 
 ;; ** Restarting and clearing spans