Move x-symbol-language to avoid eval of proof-assistant-symbol; move proof-face-specs to proof-utils

2 files changed, 1 insertions, 22 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index b1d42910..a096b295 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -71,7 +71,6 @@
 ;; ==================================================
 
 (require 'proof-utils)			;; Macros used below
-(require 'proof-compat)			;; For pg-defface-window-systems
 
 
 ;;
@@ -452,22 +451,6 @@ signals to the remote host."
   :group 'proof-general
   :prefix "proof-")
   
-(defmacro proof-face-specs (bl bd ow)
-  "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
-  `(append
-    (apply 'append
-     (mapcar 
-     (lambda (ty) (list
-		     (list (list (list 'type ty) '(class color)
-			   (list 'background 'light))
-			   (quote ,bl))
-		     (list (list (list 'type ty) '(class color)
-				 (list 'background 'dark))
-			   (quote ,bd))))
-     ;; NOTE: see proof-compat.el for possible window-system values
-     pg-defface-window-systems))
-    (list (list t (quote ,ow)))))
-
 (defface proof-queue-face 
   (proof-face-specs 
    (:background "mistyrose") ;; was "darksalmon" in PG 3.4,3.5
@@ -2598,11 +2581,6 @@ X-Symbol support is deactivated."
   :type 'string
   :group 'proof-x-symbol)
 
-(defpgcustom x-symbol-language proof-assistant-symbol
-  "Setting for x-symbol-language for the current proof assistant.
-It defaults to proof-assistant-symbol, which makes X Symbol
-look for files named x-symbol-<PA>.el.")
-
 
 
 
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 85daf3ee..1cb372fb 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -10,6 +10,7 @@
 ;; Loading note: this file is required immediately from proof.el, so
 ;; no autoloads are used here.
 
+(require 'proof-compat)			;; for pg-defface-window-systems
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;