From 46620558210c52a6ca510a77f2ae3bfc48941a05 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 23 Oct 1998 09:50:24 +0000
Subject: Replaced remaining face defs with defface calls. Removed
 font-lock-<newface> with proof-<newface> so we know where things come from
 and won't break future font locks.

---
 coq/coq-syntax.el       |  8 ++---
 generic/proof-config.el | 64 +++++++++++++++++++++++++++++++++--
 generic/proof-shell.el  |  6 ++--
 generic/proof-syntax.el | 88 +++++++++++++++++++++++++------------------------
 isa/isa-syntax.el       |  8 ++---
 lego/lego-syntax.el     |  4 +--
 6 files changed, 120 insertions(+), 58 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 4e1c8c14..ba5fc09b 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -167,10 +167,10 @@
   (list
 
    ;; lambda binders
-   (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face)
+   (list (coq-abstr-regexp "\\[" ":") 1 'proof-declaration-name-face)
 
    ;; Pi binders
-   (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face)
+   (list (coq-abstr-regexp "(" ":") 1 'proof-declaration-name-face)
    
    ;; Kinds
    (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
@@ -202,10 +202,10 @@
     coq-font-lock-terms
     (list
      (cons (ids-to-regexp coq-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp coq-tacticals) 'font-lock-tacticals-name-face)
+     (cons (ids-to-regexp coq-tacticals) 'proof-tacticals-name-face)
 
      (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)
-     (list coq-decl-with-hole-regexp 2 'font-lock-declaration-name-face)
+     (list coq-decl-with-hole-regexp 2 'proof-declaration-name-face)
      (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
      (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 148d5a63..676f317d 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -66,6 +66,23 @@ Used internally and in menu titles."
   :type 'boolean
   :group 'proof)
 
+;;
+;; Faces.
+;; We ought to test that these work sensibly:
+;;   a) with default colours
+;;   b) with -rv
+;;   c) on console 
+;;   d) on win32
+;;   e) all above with FSF Emacs and XEmacs.
+;; But it's difficult to keep track of all that!  
+;; Please report any bad/failing colour 
+;; combinations to proofgen@dcs.ed.ac.uk
+;;
+;; Some of these faces aren't used by default in Proof General,
+;; but you can use them in font lock patterns for specific
+;; script languages.
+;;
+
 (defface proof-queue-face
   '((((type x) (class color) (background light))
      (:background "mistyrose"))
@@ -73,7 +90,7 @@ Used internally and in menu titles."
      (:background "mediumvioletred"))
     (t				
      (:foreground "white" :background "black")))
-  "Face for commands in proof script waiting to be processed."
+  "*Face for commands in proof script waiting to be processed."
   :group 'proof)
 
 (defface proof-locked-face
@@ -83,9 +100,52 @@ Used internally and in menu titles."
      (:background "navy"))
     (t				
      (:underline t)))
-  "Face for locked region of proof script (processed commands)."
+  "*Face for locked region of proof script (processed commands)."
+  :group 'proof)
+
+(defface proof-declaration-name-face
+  '((((type x) (class color) (background light))   
+     (:foreground "chocolate" 
+      :bold t))
+    (((type x) (class color) (background dark))   
+     (:foreground "orange"
+      :bold t))
+    (t				
+     (:italic t :bold t)))
+  "*Face for declaration names in proof scripts."
   :group 'proof)
 
+(defface proof-tacticals-name-face
+  '((((type x) (class color) (background light))   
+     (:foreground "MediumOrchid3"))
+    (((type x) (class color) (background dark))   
+     (:foreground "orchid"))
+    (t				
+     (bold t)))
+  "*Face for names of tacticals in proof scripts."
+  :group 'proof)
+
+(defface proof-error-face 
+  '((((type x) (class color) (background light))   
+     (:background "salmon1"  
+      :bold t))
+    (((type x) (class color) (background dark))   
+     (:background "brown" 
+      :bold t))
+    (t				
+     (:bold t)))
+  "*Face for error messages from proof assistant.")
+
+(defface proof-eager-annotation-face
+  '((((type x) (class color) (background light))   
+     (:background "lemon chiffon"))
+    (((type x) (class color) (background dark))   
+     (:background "darkgoldenrod"))
+    (t				
+     (:italic t)))
+  "*Face for messages from proof assistant.")
+
+
 
 
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index eab8dc17..de92f427 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -400,7 +400,7 @@ error message. At the end it calls `proof-shell-handle-error-hook'. "
     ;;   detected by a regular expression.
   (proof-shell-handle-output
    proof-shell-error-regexp proof-shell-annotated-prompt-regexp
-   'font-lock-error-face)
+   'proof-error-face)
   (save-excursion (display-buffer proof-shell-buffer)
 		  (beep)
 
@@ -656,7 +656,7 @@ arrive."
   (let ((str (proof-shell-handle-output
 	      proof-shell-eager-annotation-start
 	      proof-shell-eager-annotation-end
-	      'font-lock-eager-annotation-face))
+	      'proof-eager-annotation-face))
 	file module)
     (proof-message str)))
 
@@ -717,7 +717,7 @@ arrive."
 	(t
 	 (proof-message message)
 	 (proof-response-buffer-display message
-					'font-lock-eager-annotation-face))))
+					'proof-eager-annotation-face))))
 
 (defun proof-shell-process-urgent-messages (str)
   "Scan the process output for urgent messages.
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 25964dac..265791db 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -37,53 +37,55 @@
 ;; font lock faces: declarations, errors, tacticals                 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; FIXME 1: these names are bad, should be proof-<blah>-face.
-;; FIXME 2: use defface here
-
-(defun proof-have-color ()
-  "Do we have support for colour?"
-  (or (and (fboundp 'device-class)
-	   (eq (device-class (frame-device)) 'color))
-      (and (fboundp 'x-display-color-p) (x-display-color-p))))
-
-(defvar font-lock-declaration-name-face 
-(progn 
-  (cond 
-   ((proof-have-color)
-    (copy-face 'bold 'font-lock-declaration-name-face)
-
-    ;; Emacs 19.28 compiles this down to
-    ;; internal-set-face-1. This is not compatible with XEmacs
-    (set-face-foreground
-     'font-lock-declaration-name-face "chocolate"))
-   (t (copy-face 'bold-italic 'font-lock-declaration-name-face)))))
+
+;; FACES have been moved to proof-config.
+;; Old code left here while testing.
+
+;(defun proof-have-color ()
+;  "Do we have support for colour?"
+;  (or (and (fboundp 'device-class)
+;	   (eq (device-class (frame-device)) 'color))
+;      (and (fboundp 'x-display-color-p) (x-display-color-p))))
+
+;(defvar font-lock-declaration-name-face 
+;(progn 
+;  (cond 
+;   ((proof-have-color)
+;    (copy-face 'bold 'font-lock-declaration-name-face)
+
+;    ;; Emacs 19.28 compiles this down to
+;    ;; internal-set-face-1. This is not compatible with XEmacs
+;    (set-face-foreground
+;     'font-lock-declaration-name-face "chocolate"))
+;   (t (copy-face 'bold-italic 'font-lock-declaration-name-face)))))
 
 ;;  (if running-emacs19
 ;;      (setq font-lock-declaration-name-face
 ;;	    (face-name 'font-lock-declaration-name-face))
 
-(defvar font-lock-tacticals-name-face
-(if (proof-have-color)
-    (let ((face (make-face 'font-lock-tacticals-name-face)))
-      (dont-compile
-	(set-face-foreground face "MediumOrchid3"))
-      face)
-  (copy-face 'bold 'font-lock-tacticals-name-face)))
-
-(defvar font-lock-error-face
-  (let ((face (make-face 'font-lock-error-face)))
-    (copy-face 'bold 'font-lock-error-face)
-    (and (proof-have-color) (set-face-background face "salmon1"))
-    face)
-  "*The face for error messages.")
-
-(defvar font-lock-eager-annotation-face
-  (let ((face (make-face 'font-lock-eager-annotation-face)))
-    (if (proof-have-color)
-	(set-face-background face "lemon chiffon")
-      (copy-face 'italic face))
-    face)
-  "*The face for urgent messages.")
+
+;(defvar font-lock-tacticals-name-face
+;(if (proof-have-color)
+;    (let ((face (make-face 'font-lock-tacticals-name-face)))
+;      (dont-compile
+;	(set-face-foreground face "MediumOrchid3"))
+;      face)
+;  (copy-face 'bold 'font-lock-tacticals-name-face)))
+
+;(defvar font-lock-error-face
+;  (let ((face (make-face 'font-lock-error-face)))
+;    (copy-face 'bold 'font-lock-error-face)
+;    (and (proof-have-color) (set-face-background face "salmon1"))
+;    face)
+;  "*The face for error messages.")
+
+;(defvar font-lock-eager-annotation-face
+;  (let ((face (make-face 'font-lock-eager-annotation-face)))
+;    (if (proof-have-color)
+;	(set-face-background face "lemon chiffon")
+;      (copy-face 'italic face))
+;    face)
+;  "*The face for urgent messages.")
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; A big hack to unfontify commas in declarations and definitions.  ;;
@@ -103,7 +105,7 @@
       (goto-char start)
       (while (search-forward "," end t)
 	(if (memq (get-char-property (- (point) 1) 'face)
-		'(font-lock-declaration-name-face
+		'(proof-declaration-name-face
 		  font-lock-function-name-face))
 	    (font-lock-remove-face (- (point) 1) (point))
 	    )))))
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 886a686b..93ad9758 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -111,10 +111,10 @@
   (list
    ;; lambda binders
    (list (concat "\%\\s-*\\(" isa-ids "\\)\\.") 1
-	 'font-lock-declaration-name-face)
+	 'proof-declaration-name-face)
 
    ;; Pi binders
-   (list (isa-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face)
+   (list (isa-abstr-regexp "(" ":") 1 'proof-declaration-name-face)
    
    ;; Kinds
    (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
@@ -143,10 +143,10 @@
     isa-font-lock-terms
     (list
      (cons (ids-to-regexp isa-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp isa-tacticals) 'font-lock-tacticals-name-face)
+     (cons (ids-to-regexp isa-tacticals) 'proof-tacticals-name-face)
 
      (list isa-goal-with-hole-regexp 2 'font-lock-function-name-face)
-     (list isa-decl-with-hole-regexp 2 'font-lock-declaration-name-face)
+     (list isa-decl-with-hole-regexp 2 'proof-declaration-name-face)
      (list isa-defn-with-hole-regexp 2 'font-lock-function-name-face)
      (list isa-save-with-hole-regexp 2 'font-lock-function-name-face))))
 
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index 5c551a6d..a70b627c 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -64,7 +64,7 @@
 
    ; lambda binders
      (list (lego-decl-defn-regexp "[:|]") 1
-	   'font-lock-declaration-name-face)
+	   'proof-declaration-name-face)
 
      ; let binders
      (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face)
@@ -72,7 +72,7 @@
 
      ; Pi and Sigma binders
      (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
-	   'font-lock-declaration-name-face)
+	   'proof-declaration-name-face)
    
      ;; Kinds
      (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
-- 
cgit v1.2.3