proof-strict-read-only: replace 'strict with t. Add proof-use-parser-cache.

1 files changed, 14 insertions, 2 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4a1bfeb7..bf45a2b1 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -175,12 +175,15 @@ done if this `proof-strict-state-preserving' is turned off (nil)."
   :type  'boolean
   :group 'proof-user-options)
 
-(defcustom proof-strict-read-only 'strict
+(defcustom proof-strict-read-only t
   "*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  '(choice (const strict) (const retract) (const nil))
+  :type  '(choice 
+	   (const :tag "Do not allow edits" t) 
+	   (const :tag "Allow edits but automatically retract first" retract)  
+	   (const :tag "Allow edits without restriction" nil))
   :set   'proof-set-value
   :group 'proof-user-options)
 
@@ -328,6 +331,15 @@ This is only useful for PG developers."
   :type 'boolean
   :group 'proof-user-options)
 
+;;; TEMPORARY FOR EXPERIMENTAL CODE:
+
+(defcustom proof-use-parser-cache nil
+  "*Non-nil to use a simple parsing cache (experimental).
+This can be helpful when editing and reprocessing large files.
+This variable exists to disable the cache in case of problems."
+  :type 'boolean
+  :group 'proof-user-options)
+
 
 ;;; NON BOOLEAN OPTIONS