Added deffaces to proof-config

2 files changed, 33 insertions, 28 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 5c82946e..148d5a63 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -30,11 +30,21 @@
 ;; The remaining variables in sections 2-5 do.
 ;;
 
+;;
+;; 0. Global constants
+;; 
 
-;; A global constant that's convenient to keep here.
-(defconst proof-mode-name "Proof-General"
+(defcustom proof-mode-name "Proof-General"
   "Root name for proof script mode.  
-Used internally and in menu titles.")
+Used internally and in menu titles."
+  :type 'string
+  :group 'proof-internal)
+
+(defcustom proof-general-home-page
+  "http://www.dcs.ed.ac.uk/home/proofgen"
+  "*Web address for Proof General"
+  :type 'string
+  :group 'proof-internal)
 
 
 
@@ -56,11 +66,26 @@ Used internally and in menu titles.")
   :type 'boolean
   :group 'proof)
 
-(defcustom proof-general-home-page
-  "http://www.dcs.ed.ac.uk/home/proofgen"
-  "*Web address for Proof General"
-  :type 'string
-  :group 'proof-internal)
+(defface proof-queue-face
+  '((((type x) (class color) (background light))
+     (:background "mistyrose"))
+    (((type x) (class color) (background dark))
+     (:background "mediumvioletred"))
+    (t				
+     (:foreground "white" :background "black")))
+  "Face for commands in proof script waiting to be processed."
+  :group 'proof)
+
+(defface proof-locked-face
+  '((((type x) (class color) (background light))   
+     (:background "lavender"))
+    (((type x) (class color) (background dark))   
+     (:background "navy"))
+    (t				
+     (:underline t)))
+  "Face for locked region of proof script (processed commands)."
+  :group 'proof)
+
 
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index a62900c0..2b6e92ae 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -148,26 +148,6 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
 (make-variable-buffer-local 'proof-locked-span)
 (make-variable-buffer-local 'proof-queue-span)
 
-(defface proof-queue-face
-  '((((type x) (class color) (background light))
-     (:background "mistyrose"))
-    (((type x) (class color) (background dark))
-     (:background "mediumvioletred"))
-    (t				
-     (:foreground "white" :background "black")))
-  "Face for commands in proof script waiting to be processed."
-  :group 'proof)
-
-(defface proof-locked-face
-  '((((type x) (class color) (background light))   
-     (:background "lavender"))
-    (((type x) (class color) (background dark))   
-     (:background "navy"))
-    (t				
-     (:underline t)))
-  "Face for locked region of proof script (processed commands)."
-  :group 'proof)
-
 (defun proof-init-segmentation ()
   (setq proof-queue-loose-end nil)
   (if (not proof-queue-span)