Allow proof-strict-read-only to be changed dyamically, add to quick opts menu in place of output highlight setting.

3 files changed, 50 insertions, 33 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 848346cd..47528236 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -152,23 +152,16 @@ directly (instead, they may only be entered as part of the script).
 
 Clever or arrogant users may want to avoid this test, which is
 done if this `proof-strict-state-preserving' is turned off (nil)."
-  :type 'boolean
+  :type  'boolean
   :group 'proof-user-options)
 
 (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
-you a reprimand!).
-
-If you change proof-strict-read-only during a session, you must 
-use the \"Restart\" button (or \\[proof-shell-restart]) before
-you can see the effect in buffers.
-
-The default value for proof-strict-read-only depends on which
-version of Emacs you are using.  In GNU Emacs, strict read only is buggy
-when it used in conjunction with font-lock, so it is disabled by default."
-  :type 'boolean
+you a reprimand!)."
+  :type  'boolean
+  :set   'proof-set-value
   :group 'proof-user-options)
 
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 972e0aba..3587261e 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -181,9 +181,9 @@ If in three window or multiple frame mode, display two buffers."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
-;;; Contents of the menus
-;;;
+;;
+;; Contents of sub menus
+;;
 
 (defvar proof-help-menu
   '("Help"
@@ -233,19 +233,26 @@ If in three window or multiple frame mode, display two buffers."
   "Proof General buffer menu.")
 
 
-;; Make the togglers used in options menu below
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; "Quick" (or main) options
+;;
+
+;; First, make the togglers used in options menu below
 
 (proof-deftoggle proof-three-window-mode)
 (proof-deftoggle proof-script-fly-past-comments)
 (proof-deftoggle proof-delete-empty-windows)
 (proof-deftoggle proof-shrink-windows-tofit)
 (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle)
-(proof-deftoggle proof-output-fontify-enable proof-output-fontify-toggle)
+;; (proof-deftoggle proof-output-fontify-enable proof-output-fontify-toggle)
 (proof-deftoggle proof-disappearing-proofs)
+(proof-deftoggle proof-strict-read-only)
 
 (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
 (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle)
 
+;; Here is the menu
 
 (defvar proof-quick-opts-menu
   (cons 
@@ -260,10 +267,15 @@ If in three window or multiple frame mode, display two buffers."
      ["Disppearing Proofs" proof-disappearing-proofs-toggle 
       :style toggle
       :selected proof-disappearing-proofs]
-     ["Output Highlighting" proof-output-fontify-toggle
-      :active t
+
+;     ["Output Highlighting" proof-output-fontify-toggle
+;      :active t
+;      :style toggle
+;      :selected proof-output-fontify-enable]
+
+     ["Strict read only" proof-strict-read-only-toggle
       :style toggle
-      :selected proof-output-fontify-enable]
+      :selected proof-strict-read-only]
 
      ;; X-Symbol and MM are minor modes which PG settings
      ;; enable by default for PG buffers
@@ -334,7 +346,8 @@ If in three window or multiple frame mode, display two buffers."
    'proof-electric-terminator-enable
    'proof-script-fly-past-comments
    'proof-disappearing-proofs 
-   'proof-output-fontify-enable
+   ;;'proof-output-fontify-enable
+   'proof-strict-read-only
    (proof-ass-sym x-symbol-enable)
    (proof-ass-sym mmm-enable)
    'proof-toolbar-enable
@@ -372,6 +385,13 @@ If in three window or multiple frame mode, display two buffers."
   (interactive)
   (apply 'pg-custom-reset-vars (proof-quick-opts-vars)))
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Main menu
+;;
+
+
 (defconst proof-config-menu
   (list "----"
 	;; buffer menu might better belong in toolbar menu?
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 93a0b400..332c35be 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -197,21 +197,25 @@ scripting buffer may have an active queue span.")
 
 ;; ** Getters and setters
 
-(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."
-  ;; Note: perhaps the queue region should always be locked strictly.
-  (if proof-strict-read-only
+(defun proof-span-read-only (span &optional always)
+  "Make span be read-only according to `proof-strict-read-only' or ALWAYS."
+  (if (or always proof-strict-read-only)
       (span-read-only span)
+    (span-read-write span)
     (span-write-warning span)))
 
-;; not implemented yet: presently must toggle via restarting scripting
-;; (defun proof-toggle-strict-read-only ()
-;;  "Toggle proof-strict-read-only, changing current spans."
-;;  (interactive)
-;;   map-spans blah
-;;  )
-
+(defun proof-strict-read-only ()
+  "Set locked spans in script buffers according to `proof-strict-read-only'."
+  ;; NB: this implements the behaviour that read-only is synchronized
+  ;; in all script buffers to follow the current setting of 
+  ;; `proof-strict-read-only'.  Another possibility would be to
+  ;; just change for local buffer, while at the same time changing
+  ;; the default/global setting.   This would be consistent with
+  ;; behaviour of "expensive" x-symbol/mmm options.
+  (interactive)
+  (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
+		     (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))
@@ -270,7 +274,7 @@ Also clear list of script portions."
       (span-raise proof-queue-span))
   (set-span-property proof-queue-span 'start-closed t)
   (set-span-property proof-queue-span 'end-open t)
-  (proof-span-read-only proof-queue-span)
+  (proof-span-read-only proof-queue-span 'always)
   (set-span-property proof-queue-span 'face 'proof-queue-face)
   (detach-span proof-queue-span)
   ;; Initialise locked span, remove it from buffer