aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-13 05:27:12 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-13 05:27:12 +0000
commite5aba6d81e99a4e37026445cc63be52aeed1729a (patch)
tree4d3419751881690455c316720ec1c47d994be230 /generic
parent670761dd6bd6321d65beeacdc81d68c0a2ebe92b (diff)
Added proof-boring-face (default appearance is same as proof-debug-face). Comment.
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el12
1 files changed, 11 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 0cd7058d..11005b62 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -500,6 +500,16 @@ Warning messages can come from proof assistant or from Proof General itself."
"*Face for debugging messages from Proof General."
:group 'proof-faces)
+(defface proof-boring-face
+ '((((type x) (class color) (background light))
+ (:foreground "Gray65"))
+ (((type x) (class color) (background dark))
+ (:background "Gray30"))
+ (t
+ (:italic t)))
+ "*Face for boring text in proof assistant output."
+ :group 'proof-faces)
+
@@ -1613,7 +1623,7 @@ for parsing the is disabled."
:type 'character
:group 'proof-goals)
-;; FIXME: remove this setting after 3.0, by matching on
+;; FIXME: remove this setting for 3.2, by matching on
;; completed-regexp as an extra step, after errors/interrupt,
;; but as well as ordinary output.
(defcustom proof-goals-display-qed-message nil