Make proof-assistant-settings follow currently available dynamic settings, and keep possibly customized variables bound. Closes Trac #387.

4 files changed, 14 insertions, 10 deletions

diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 798e1e78..c8bac3a5 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -183,7 +183,7 @@ Usage: (defpgdefault SYM VALUE)"
       (error "defpacustom: missing :type keyword or wrong :type value"))
 
     ;; Error in case a defpacustom is repeated.
-    (when (assoc name proof-assistant-settings)
+    (when (assq name proof-assistant-settings)
       (error "defpacustom: Proof assistant setting %s re-defined!"
 	     name))
 
@@ -204,7 +204,7 @@ Usage: (defpgdefault SYM VALUE)"
 	   (proof-assistant-settings-cmd (quote ,name)))))))
     (setq proof-assistant-settings
 	  (cons (list name setting (eval type) descr)
-		(assq-delete-all name proof-assistant-settings)))))
+		proof-assistant-settings))))
 
 ;;;###autoload
 (defmacro defpacustom (name val &rest args)
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index f4140ab5..102212ee 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -202,7 +202,7 @@ This variable can be used for instance specific functions which want
 to examine `proof-shell-last-output'.")
 
 (defvar proof-assistant-settings nil
- "A list of default values kept in Proof General for current proof assistant.
+ "Settings kept in Proof General for current proof assistant.
 A list of lists (SYMBOL SETTING TYPE DESCR) where SETTING is a string value
 to send to the proof assistant using the value of SYMBOL and
 and the function `proof-assistant-format'.  The TYPE item determines
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 5c0bfeda..cc4e850e 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -925,10 +925,13 @@ This will configure dynamic settings used in the current prover session
 and extend `proof-assistant-settings'.
 We first clear the dynamic settings from `proof-assistant-settings'."
   (when (and proof-use-pgip-askprefs proof-shell-issue-pgip-cmd)
-    (dolist (setting proof-assistant-settings)
-      (let ((name (car setting)))
-	(if (get name 'pgdynamic)
-	    (undefpgcustom name))))
+    (let (newsettings)
+      (dolist (setting proof-assistant-settings)
+	(let ((name (car setting)))
+	  (if (get name 'pgdynamic)
+	      (undefpgcustom name)
+	    (push setting newsettings))))
+      (setq proof-assistant-settings newsettings))
     (pg-pgip-askprefs)))
 
 
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 3918b7ce..45545f29 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -52,7 +52,9 @@
 ;;  "defvar treated as defconst" in XEmacs)
 (defun pg-custom-undeclare-variable (symbol)
   "Remove a custom setting SYMBOL.
-Done by `makunbound' and removing all properties mentioned by custom library."
+Done by removing all properties mentioned by custom library.
+The symbol itself is left defined, in case it has been changed
+in the current Emacs session."
   (mapc (lambda (prop) (remprop symbol prop))
 	  '(default
 	     standard-value
@@ -72,8 +74,7 @@ Done by `makunbound' and removing all properties mentioned by custom library."
 	     custom-version
 	     saved-value
 	     theme-value
-	     theme-face))
-  (makunbound symbol))
+	     theme-face)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;