From af1e37834fca25210821a558b638e98309643293 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 3 Nov 1998 11:47:13 +0000
Subject: fixed bug with font-lock face names

---
 coq/coq-syntax.el       |  8 ++++----
 generic/proof-config.el | 20 ++++++++++++--------
 isa/isa-syntax.el       |  8 ++++----
 lego/lego-syntax.el     |  6 +++---
 4 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e0ddba66..16f2a15f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -167,10 +167,10 @@
   (list
 
    ;; lambda binders
-   (list (coq-abstr-regexp "\\[" ":") 1 ''proof-declaration-name-face)
+   (list (coq-abstr-regexp "\\[" ":") 1 'proof-declaration-name-face)
 
    ;; Pi binders
-   (list (coq-abstr-regexp "(" ":") 1 ''proof-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 (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face)
-     (cons (proof-ids-to-regexp coq-tacticals) ''proof-tacticals-name-face)
+     (cons (proof-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 ''proof-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 686f6a98..8d484171 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -124,12 +124,14 @@ If ignore, point is never moved after toolbar movement commands."
       :bold t))
     (t				
      (:italic t :bold t)))
-  "*Face for declaration names in proof scripts.
-
-Don't forget to *double* quote this face for font-lock. FSF Emacs
-20.2's version only supports *expressions* for faces."
+  "*Face for declaration names in proof scripts."
   :group 'proof-faces)
 
+(defconst proof-declaration-name-face 'proof-declaration-name-face
+  "Expression that evaluates to a face.
+Required so that 'proof-declaration-name-face is a proper facename in
+both XEmacs 20.4 and Emacs 20.2's version of font-lock.")
+
 (defface proof-tacticals-name-face
   '((((type x) (class color) (background light))   
      (:foreground "MediumOrchid3"))
@@ -137,12 +139,14 @@ Don't forget to *double* quote this face for font-lock. FSF Emacs
      (:foreground "orchid"))
     (t				
      (bold t)))
-  "*Face for names of tacticals in proof scripts.
-
-Don't forget to *double* quote this face for font-lock. FSF Emacs
-20.2's version only supports *expressions* for faces."
+  "*Face for names of tacticals in proof scripts."
   :group 'proof-faces)
 
+(defconst proof-tacticals-name-face 'proof-tacticals-name-face
+  "Expression that evaluates to a face.
+Required so that 'proof-declaration-name-face is a proper facename in
+both XEmacs 20.4 and Emacs 20.2's version of font-lock.")
+
 (defface proof-error-face 
   '((((type x) (class color) (background light))   
      (:background "salmon1"  
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 8a59c076..bef89b5b 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -110,10 +110,10 @@
   (list
    ;; lambda binders
    (list (concat "\%\\s-*\\(" isa-ids "\\)\\.") 1
-	 ''proof-declaration-name-face)
+	 'proof-declaration-name-face)
 
    ;; Pi binders
-   (list (isa-abstr-regexp "(" ":") 1 ''proof-declaration-name-face)
+   (list (isa-abstr-regexp "(" ":") 1 'proof-declaration-name-face)
    
    ;; Kinds
    (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
@@ -148,10 +148,10 @@
     isa-font-lock-terms
     (list
      (cons (proof-ids-to-regexp isa-keywords) 'font-lock-keyword-face)
-     (cons (proof-ids-to-regexp isa-tacticals) ''proof-tacticals-name-face)
+     (cons (proof-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 ''proof-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 34608afb..64399546 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -64,7 +64,7 @@
 
    ; lambda binders
      (list (lego-decl-defn-regexp "[:|?]") 1
-	   ''proof-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
-	   ''proof-declaration-name-face)
+	   'proof-declaration-name-face)
    
      ;; Kinds
      (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
@@ -96,7 +96,7 @@
     lego-font-lock-terms
     (list
      (cons (proof-ids-to-regexp lego-keywords) 'font-lock-keyword-face)
-     (cons (proof-ids-to-regexp lego-tacticals) ''proof-tacticals-name-face)
+     (cons (proof-ids-to-regexp lego-tacticals) 'proof-tacticals-name-face)
      (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
      (list lego-save-with-hole-regexp 2 'font-lock-function-name-face))))
      
-- 
cgit v1.2.3