1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
|
;;; proof-faces.el --- Faces for Proof General
;;
;; Copyright (C) 2009 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;; Commentary:
;;
;; In an ideal world, faces should work sensibly:
;;
;; a) with default colours
;; b) with -rv
;; c) on console
;; d) on different Emacsen/architectures (win32, mac, etc)
;;
;; But it's difficult to keep track of all that!
;; Please report any bad/failing colour
;; combinations (with suggested improvements) at
;; http://proofgeneral.inf.ed.ac.uk/trac
;;
;; 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.
;;; Code:
(defgroup proof-faces nil
"Faces used by Proof General."
:group 'proof-general
:prefix "proof-")
;; TODO: get rid of this list. Does 'default work widely enough
;; by now?
(defconst pg-defface-window-systems
'(x ;; bog standard
mswindows ;; Windows
w32 ;; Windows
gtk ;; gtk emacs (obsolete?)
mac ;; used by Aquamacs
carbon ;; used by Carbon XEmacs
ns ;; NeXTstep Emacs (Emacs.app)
x-toolkit) ;; possible catch all (but probably not)
"A list of possible values for variable `window-system'.
If you are on a window system and your value of variable `window-system' is
not listed here, you may not get the correct syntax colouring behaviour.")
(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))))
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
(:background "mediumvioletred")
(:foreground "white" :background "black"))
"*Face for commands in proof script waiting to be processed."
:group 'proof-faces)
(defface proof-locked-face
(proof-face-specs
;; This colour is quite subjective and may be best chosen according
;; to the type of display you have.
(:background "#eaf8ff")
(:background "darkblue")
(:underline t))
"*Face for locked region of proof script (processed commands)."
:group 'proof-faces)
(defface proof-declaration-name-face
(proof-face-specs
(:foreground "chocolate" :bold t)
(:foreground "orange" :bold t)
(:italic t :bold t))
"*Face for declaration names in proof scripts.
Exactly what uses this face depends on the proof assistant."
:group 'proof-faces)
(defface proof-tacticals-name-face
(proof-face-specs
(:foreground "MediumOrchid3")
(:foreground "orchid")
(bold t))
"*Face for names of tacticals in proof scripts.
Exactly what uses this face depends on the proof assistant."
:group 'proof-faces)
(defface proof-tactics-name-face
(proof-face-specs
(:foreground "darkblue")
(:foreground "mediumpurple")
(:underline t))
"*Face for names of tactics in proof scripts.
Exactly what uses this face depends on the proof assistant."
:group 'proof-faces)
(defface proof-error-face
(proof-face-specs
(:background "rosybrown1") ; a drab version of misty rose
(:background "brown")
(:bold t))
"*Face for error messages from proof assistant."
:group 'proof-faces)
(defface proof-warning-face
(proof-face-specs
(:background "lemon chiffon")
(:background "orange2")
(:italic t))
"*Face for warning messages.
Warning messages can come from proof assistant or from Proof General itself."
:group 'proof-faces)
(defface proof-eager-annotation-face
(proof-face-specs
(:background "palegoldenrod")
(:background "darkgoldenrod")
(:italic t))
"*Face for important messages from proof assistant."
:group 'proof-faces)
(defface proof-debug-message-face
(proof-face-specs
(:foreground "Gray65")
(:background "Gray30")
(:italic t))
"*Face for debugging messages from Proof General."
:group 'proof-faces)
(defface proof-boring-face
(proof-face-specs
(:foreground "Gray75")
(:background "Gray30")
(:italic t))
"*Face for boring text in proof assistant output."
:group 'proof-faces)
(defface proof-mouse-highlight-face
(proof-face-specs
(:background "lightblue")
(:background "darkslateblue")
(:italic t))
"*General mouse highlighting face used in script buffer."
:group 'proof-faces)
(defface proof-command-mouse-highlight-face
(proof-face-specs
(:background "gold1")
(:background "gold4")
(:italic t))
"*Mouse highlighting face for atomic regions (usually commands) in script buffer."
:group 'proof-faces)
(defface proof-region-mouse-highlight-face
(proof-face-specs
(:background "yellow2")
(:background "yellow3")
(:italic t))
"*Mouse highlighting face for compound regions (usually proofs) in script buffer."
:group 'proof-faces)
(defface proof-highlight-dependent-face
(proof-face-specs
(:background "orange")
(:background "darkorange")
(:italic t))
"*Face for showing (backwards) dependent parts."
:group 'proof-faces)
(defface proof-highlight-dependency-face
(proof-face-specs
(:background "khaki")
(:background "peru")
(:italic t))
"*Face for showing (forwards) dependencies."
:group 'proof-faces)
(defface proof-active-area-face
(proof-face-specs
(:background "lightyellow" :box (:line-width 2 :color "grey75" :style released-button))
(:background "darkyellow" :underline t)
(:underline t))
"*Face for showing active areas (clickable regions), outside of subterm markup."
:group 'proof-faces)
(defface proof-script-sticky-error-face
(proof-face-specs
(:background "indianred1")
(:background "indianred3")
(:underline t))
"Proof General face for marking an error in the proof script. "
:group 'proof-faces)
(defface proof-script-highlight-error-face
(proof-face-specs
(:background "indianred1" :bold t)
(:background "indianred3" :bold t)
(:underline t :bold t))
"Proof General face for highlighting an error in the proof script. "
:group 'proof-faces)
;;; Compatibility: these are required for use in GNU Emacs/font-lock-keywords
(defconst proof-face-compat-doc "Evaluates to a face name, for compatibility.")
(defconst proof-queue-face 'proof-queue-face proof-face-compat-doc)
(defconst proof-locked-face 'proof-locked-face proof-face-compat-doc)
(defconst proof-declaration-name-face 'proof-declaration-name-face proof-face-compat-doc)
(defconst proof-tacticals-name-face 'proof-tacticals-name-face proof-face-compat-doc)
(defconst proof-tactics-name-face 'proof-tactics-name-face proof-face-compat-doc)
(defconst proof-error-face 'proof-error-face proof-face-compat-doc)
(defconst proof-script-sticky-error-face 'proof-script-sticky-error-face proof-face-compat-doc)
(defconst proof-script-highlight-error-face 'proof-script-highlight-error-face proof-face-compat-doc)
(defconst proof-warning-face 'proof-warning-face proof-face-compat-doc)
(defconst proof-eager-annotation-face 'proof-eager-annotation-face proof-face-compat-doc)
(defconst proof-debug-message-face 'proof-debug-message-face proof-face-compat-doc)
(defconst proof-boring-face 'proof-boring-face proof-face-compat-doc)
(defconst proof-mouse-highlight-face 'proof-mouse-highlight-face proof-face-compat-doc)
(defconst proof-command-mouse-highlight-face 'proof-command-mouse-highlight-face proof-face-compat-doc)
(defconst proof-region-mouse-highlight-face 'proof-region-mouse-highlight-face proof-face-compat-doc)
(defconst proof-highlight-dependent-face 'proof-highlight-dependent-face proof-face-compat-doc)
(defconst proof-highlight-dependency-face 'proof-highlight-dependency-face proof-face-compat-doc)
(defconst proof-active-area-face 'proof-active-area-face proof-face-compat-doc)
(defconst proof-script-error-face 'proof-script-errror-face-compat-doc)
(provide 'proof-faces)
;;; proof-faces.el ends here
|
