diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-db.el | 29 | ||||
| -rw-r--r-- | coq/coq.el | 16 |
2 files changed, 26 insertions, 19 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index 758177c9..4677387b 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -325,26 +325,31 @@ 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 +;; This is so quite ugly, better have our own face. ;; (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")) +;; '((t :inherit custom-button :background "dark gray" +;; ;; -1 avoids messing with line and column sizes +;; :box (:line-width (-1 . -1) :style key-pressed))) ;; "" ;; :group 'proof-faces) (defface coq-button-face - '((t . (:background "light gray"))) - "" + '( + (((class color) (background light)) . (:background "light gray")) + (((class color) (background dark)) . (:background "gray" :foreground "black"))) + "Coq face for the (un)folding hypothesis button" :group 'proof-faces) (defface coq-button-face-pressed - '((t . (:background "dark gray"))) - "" + '((((class color) (background light)) . (:background "gray")) + (((class color) (background dark)) . (:background "dim gray" :foreground "black"))) + "Coq face for the (un)folding hypothesis button" + :group 'proof-faces) + +(defface coq-button-face-active + '((((class color) (background light)) . (:background "black" :foreground "white")) + (((class color) (background dark)) . (:background "grey24" :foreground "black"))) + "Coq face for the (un)folding hypothesis button" :group 'proof-faces) (defconst coq-solve-tactics-face 'coq-solve-tactics-face @@ -1417,13 +1417,13 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") (propertize "-" 'face 'coq-button-face - 'mouse-face 'coq-button-face-pressed)) + 'mouse-face 'coq-button-face-active)) (defun coq-hypcross-folded-string() (propertize "+" - 'face 'coq-button-face - 'mouse-face 'coq-button-face-pressed)) + 'face 'coq-button-face-pressed + 'mouse-face 'coq-button-face-active)) ;; hypcross is displayerd with a "-" when unfolded and a "+" when unfolded. ;; It is highlighted when hovered, is clickable and have a special @@ -1444,7 +1444,7 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") ;(overlay-put ov 'width .6) ;(overlay-put ov 'height -1) (when (eq coq-hypcross-hovering-help t) - (overlay-put ov 'help-echo "mouse-3: unfold; mouse-2 copy name"))) + (overlay-put ov 'help-echo "MOUSE-1: (un)fold ; MOUSE-2 copy hyp name at point"))) ov)) ;; Once we have created the 3 overlays, each recieves a reference to the 2 @@ -1705,7 +1705,7 @@ Used on hyptohesis overlays in goals buffer mainly." ) (overlay-put hyp-overlay 'evaporate t) (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face) - (overlay-put hyp-overlay 'help-echo "mouse-3: unfold; mouse-2 copy name") + (overlay-put hyp-overlay 'help-echo "MOUSE-1: unfold; MOUSE-2 copy name at point") (overlay-put hyp-overlay 'hyp-name h) (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map) (overlay-put hypcross-ov 'display (coq-hypcross-folded-string))))) @@ -3022,18 +3022,20 @@ Completion is on a quasi-exhaustive list of Coq tacticals." ;; point. (when coq-hypname-map (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypcross-map [(return)] 'coq-toggle-fold-hyp-at-point) (define-key coq-hypname-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) ;; Default binding: clicking on the cross to folds/unfold hyp. ;; Click on it with button 2 copies the names at current point. (when coq-hypname-map (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse) - (define-key coq-hypcross-map [return] 'coq-toggle-fold-hyp-at-point) + (define-key coq-hypcross-map [(return)] 'coq-toggle-fold-hyp-at-point) (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) ;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds it, with ;; button 2 it copies hyp name at current point. (when coq-hidden-hyp-map - (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hidden-hyp-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypcross-map [(return)] 'coq-toggle-fold-hyp-at-point) (define-key coq-hidden-hyp-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) ;;;;;;;;;;;;;;;;;;;;;;;; |