diff options
| -rw-r--r-- | coq/coq-db.el | 29 | ||||
| -rw-r--r-- | coq/coq-system.el | 26 | ||||
| -rw-r--r-- | coq/coq.el | 18 |
3 files changed, 40 insertions, 33 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-system.el b/coq/coq-system.el index 01b9b1d5..804831da 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -652,27 +652,27 @@ Does nothing if `coq-use-project-file' is nil." ;; need to make this hook local. ;; hack-local-variables-hook seems to hack local and dir local vars. (add-hook 'coq-mode-hook - '(lambda () - (add-hook 'hack-local-variables-hook - 'coq-load-project-file - nil t))) + (lambda () + (add-hook 'hack-local-variables-hook + 'coq-load-project-file + nil t))) ; detecting coqtop args should happen at the last moment before ; calling the process. In particular it should ahppen after that ; proof-prog-name-ask is performed, this hook is at the right place. (add-hook 'proof-shell-before-process-hook - '(lambda () - ;; It seems coq-prog-name and proof-prog-name are not correctly linked - ;; so let us make sure they are the same before computing options - (setq coq-prog-name proof-prog-name) - (setq coq-prog-args (coq-prog-args)))) + (lambda () + ;; It seems coq-prog-name and proof-prog-name are not correctly linked + ;; so let us make sure they are the same before computing options + (setq coq-prog-name proof-prog-name) + (setq coq-prog-args (coq-prog-args)))) ;; smie's parenthesis blinking is too slow, let us have the default one back (add-hook 'coq-mode-hook - '(lambda () - (when (and (fboundp 'show-paren--default) - (boundp 'show-paren-data-function)) - (setq show-paren-data-function 'show-paren--default)))) + (lambda () + (when (and (fboundp 'show-paren--default) + (boundp 'show-paren-data-function)) + (setq show-paren-data-function 'show-paren--default)))) @@ -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))))) @@ -2859,7 +2859,7 @@ Also insert holes at insertion positions." (setq cmd (read-string "Build match for type: ")) (let* ((thematch (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd "."))) - (match (replace-regexp-in-string "=> \n" "=> #\n" thematch))) + (match (replace-regexp-in-string "=> *\n" "=> #\n" thematch))) ;; if error, it will be displayed in response buffer (see def of ;; proof-shell-invisible-cmd-get-result), otherwise: (unless (proof-string-match coq-error-regexp match) @@ -3030,18 +3030,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)) ;;;;;;;;;;;;;;;;;;;;;;;; |