From 46b0f043d73db801a7fd340dca70d918532e4221 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 31 Jan 2011 12:47:43 +0000
Subject: Only make settings commands for dynamic settings which differ from
 their defaults

---
 generic/pg-pamacs.el  |  6 ++++++
 generic/proof-menu.el | 21 +++++++++++++--------
 2 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index c8bac3a5..de05c04d 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -65,6 +65,12 @@ This macro should only be invoked once a specific prover is engaged."
   `(symbol-value (intern (concat (symbol-name proof-assistant-symbol) "-"
 				 (symbol-name ',sym)))))
 
+(defun proof-ass-differs-from-default (sym)
+  "Return non-nil if SYM for current prover differs from its customize standard value."
+  (let ((pasym (proof-ass-symv sym)))
+    (not (equal (eval (car (get pasym 'standard-value)))
+		(symbol-value pasym)))))
+
 (defun proof-defpgcustom-fn (sym args)
   "Define a new customization variable <PA>-sym for current proof assistant.
 Helper for macro `defpgcustom'."
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index cc4e850e..798dba89 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -937,7 +937,7 @@ We first clear the dynamic settings from `proof-assistant-settings'."
 
 (defun proof-assistant-settings-cmd (setting)
   "Return string for making SETTING in Proof General customization."
-  (let ((expr (assoc setting proof-assistant-settings)))
+  (let ((expr (assq setting proof-assistant-settings)))
     (if (and expr (cadr expr))
 	(proof-assistant-format
 	 (cadr expr)
@@ -945,13 +945,18 @@ We first clear the dynamic settings from `proof-assistant-settings'."
 
 (defun proof-assistant-settings-cmds ()
   "Return strings for settings kept in Proof General customizations."
-  (when proof-assistant-settings
-    (mapcar (lambda (expr)
-	      (if (cadr expr)  ;; setting has PA string?
-		  (proof-assistant-format
-		   (cadr expr)
-		   (eval (proof-ass-symv (car expr))))))
-	    proof-assistant-settings)))
+  (let (cmds)
+    (dolist (setting proof-assistant-settings)
+      (let ((sym       (car setting))
+	    (pacmd     (cadr setting))) 
+	(if (and pacmd
+		 (or (not (get sym 'pgdynamic))
+		     (proof-ass-differs-from-default sym)))
+	    (push (proof-assistant-format pacmd
+					  (eval (proof-ass-symv sym)))
+		  cmds))))
+    cmds))
+
 
 (defvar proof-assistant-format-table
   (list
-- 
cgit v1.2.3