diff options
| -rw-r--r-- | CHANGES | 15 | ||||
| -rw-r--r-- | coq/coq.el | 43 |
2 files changed, 36 insertions, 22 deletions
@@ -106,6 +106,21 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Experimental: colorize hypothesis names and some parts of error and warning messages. For readability. +*** mouse Queries + + This remaps standard emacs key bindings (faces and buffers menus + popup), so this is not enabled by default, use (setq + coq-remap-mouse-1 t) to enable. + + - (control mouse-1) on an identifier sends a Print query on that id. + - (shift mouse-1) on an identifier sends a About query on that id. + - (control shift mouse-1) on an identifier sends a Check query on + that id. + + As most of the bindings, they are active in the three buffer + (script, goals, response). + + * Changes of Proof General 4.2 from Proof General 4.1 ** Generic/misc changes @@ -2166,28 +2166,27 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)] 'proof-store-goals-win) (define-key coq-response-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) -(eval-when-compile - (when coq-remap-mouse-1 - (define-key proof-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-mode-map [(control mouse-1)] '(lambda () (interactive))) - (define-key proof-mode-map [(shift mouse-1)] '(lambda () (interactive))) - (define-key proof-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-mode-map [(control shift mouse-1)] '(lambda () (interactive))) - - (define-key proof-response-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-response-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-response-mode-map [(control mouse-1)] '(lambda () (interactive))) - (define-key proof-response-mode-map [(shift mouse-1)] '(lambda () (interactive))) - (define-key proof-response-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-response-mode-map [(control shift mouse-1)] '(lambda () (interactive))) - - (define-key proof-goals-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-goals-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-goals-mode-map [(control mouse-1)] '(lambda () (interactive))) - (define-key proof-goals-mode-map [(shift mouse-1)] '(lambda () (interactive))) - (define-key proof-goals-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) - (define-key proof-goals-mode-map [(control shift mouse-1)] '(lambda () (interactive))))) +(when coq-remap-mouse-1 + (define-key proof-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-mode-map [(control mouse-1)] '(lambda () (interactive))) + (define-key proof-mode-map [(shift mouse-1)] '(lambda () (interactive))) + (define-key proof-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-mode-map [(control shift mouse-1)] '(lambda () (interactive))) + + (define-key proof-response-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-response-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-response-mode-map [(control mouse-1)] '(lambda () (interactive))) + (define-key proof-response-mode-map [(shift mouse-1)] '(lambda () (interactive))) + (define-key proof-response-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-response-mode-map [(control shift mouse-1)] '(lambda () (interactive))) + + (define-key proof-goals-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-goals-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-goals-mode-map [(control mouse-1)] '(lambda () (interactive))) + (define-key proof-goals-mode-map [(shift mouse-1)] '(lambda () (interactive))) + (define-key proof-goals-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) + (define-key proof-goals-mode-map [(control shift mouse-1)] '(lambda () (interactive)))) ;;;;;;;;;;;;;;;;;;;;;;;; ;; error handling |