diff options
author | 1998-10-23 09:50:24 +0000 | |
---|---|---|
committer | 1998-10-23 09:50:24 +0000 | |
commit | 46620558210c52a6ca510a77f2ae3bfc48941a05 (patch) | |
tree | 3a9184e10e81a101311c5a67fe2b899484cea67a /generic | |
parent | 2e7671f6c80becf896ca1ba4f0f5cb8e05e3b281 (diff) |
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.
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-config.el | 64 | ||||
-rw-r--r-- | generic/proof-shell.el | 6 | ||||
-rw-r--r-- | generic/proof-syntax.el | 88 |
3 files changed, 110 insertions, 48 deletions
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)) ))))) |