1 files changed, 45 insertions, 13 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index 0d9c0a6e..dccdca52 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -1,9 +1,18 @@
-;;; coq-db.el --- coq keywords database utility functions
-;;
+;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*-
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
+
 ;; Author: Pierre Courtieu <courtieu@lri.fr>
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;;
+
 ;;; Commentary:
 ;;
 ;; We store all information on keywords (tactics or command) in big
@@ -284,19 +293,20 @@ See `coq-syntax-db' for DB structure."
 (defface coq-solve-tactics-face
   (proof-face-specs
    (:foreground "red") ; pour les fonds clairs
-   (:foreground "red") ; pour les fond foncés
+   (:foreground "red1") ; pour les fonds foncés
    ()) ; pour le noir et blanc
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
-;;A new face for cheating tactics 
-;; FIXMe: the background color disappear when locked region overrides it.
-;; this is hard to fix without re-colorizing afterward.
+;;A face for cheating tactics 
+;; We use :box in addition to :background because box remains visible in
+;; locked-region. :reverse-video is another solution.
 (defface coq-cheat-face
-  (proof-face-specs
-   (:background "red") ; pour les fonds clairs
-   (:background "red") ; pour les fond foncés
-   ()) ; pour le noir et blanc
+  '(;(((class color) (background light)) . (:inverse-video t :foreground "red" :background "black"))
+    ;(((class color) (background dark)) . (:inverse-video t :foreground "red1"))
+    (((class color) (background light)) . (:box (:line-width -1 :color "red" :style nil) :background "red"))
+    (((class color) (background dark)) . (:box (:line-width -1 :color "red1" :style nil) :background "red1"))
+    (t . ())) ; monocolor or greyscale: no highlight
   "Face for names of cheating tactics in proof scripts."
   :group 'proof-faces)
 
@@ -306,7 +316,7 @@ See `coq-syntax-db' for DB structure."
   :group 'proof-faces)
 
 (defface coq-symbol-face
-  '((t :inherit default-face :bold coq-bold-unicode-binders))
+  '((t :inherit font-lock-type-face :bold coq-bold-unicode-binders))
   "Face for unicode binders, by default a bold version of `font-lock-type-face'."
   :group 'proof-faces)
 
@@ -320,6 +330,28 @@ See `coq-syntax-db' for DB structure."
   "Face used for `ltac:', `constr:', and `uconstr:' headers."
   :group 'proof-faces)
 
+;; This messes columns, can't figure out why putting this face makes the overlay
+;; larger than a character
+;; (defface coq-button-face
+;;   '((t :inherit custom-button :background "dark gray"))
+;;   ""
+;;   :group 'proof-faces)
+
+;; (defface coq-button-face-pressed
+;;   '((t :inherit custom-button-pressed :background "light gray"))
+;;   ""
+;;   :group 'proof-faces)
+
+(defface coq-button-face
+  '((t . (:background "light gray")))
+  ""
+  :group 'proof-faces)
+
+(defface coq-button-face-pressed
+  '((t . (:background "dark gray")))
+  ""
+  :group 'proof-faces)
+
 (defconst coq-solve-tactics-face 'coq-solve-tactics-face
   "Expression that evaluates to a face.
 Required so that 'coq-solve-tactics-face is a proper facename")