Fixing hypothesis folding GUI.

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
diff --git a/coq/coq.el b/coq/coq.el
index c1f52d38..cd9f7294 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;