diff options
-rw-r--r-- | generic/pg-goals.el | 2 | ||||
-rw-r--r-- | generic/pg-vars.el | 2 | ||||
-rw-r--r-- | generic/proof-menu.el | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 1dc079cb..55a64bfc 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -56,7 +56,7 @@ May enable proof-by-pointing or similar features. (define-key proof-goals-mode-map [q] 'bury-buffer) ;; TODO: use standard Emacs button behaviour here (cf Info mode) (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action) -(define-key proof-goals-mode-map [C-mouse-3] +(define-key proof-goals-mode-map [C-M-mouse-3] 'proof-undo-and-delete-last-successful-command) diff --git a/generic/pg-vars.el b/generic/pg-vars.el index 36f7f6d6..45040c94 100644 --- a/generic/pg-vars.el +++ b/generic/pg-vars.el @@ -269,7 +269,7 @@ Internal variable dynamically bound.") ([(control c) (control ?.)] . proof-goto-end-of-locked) ([(control c) (control f)] . proof-find-theorems) ([(control c) (control o)] . proof-display-some-buffers) - ([C-M-mouse-1] . pg-identifier-under-mouse-query)) ; holes overrides this + ([(control shift mouse-1)] . pg-identifier-under-mouse-query)) "List of key bindings made for all proof general buffers. Elements of the list are tuples `(k . f)' where `k' is a key binding (vector) and `f' the designated function." diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 814804c6..693a4ad2 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -123,7 +123,7 @@ without adjusting window layout." ;; C-c C-. is proof-goto-end-of-locked in universal-keys (define-key map [(control c) (control return)] 'proof-goto-point) (define-key map [(control c) ?v] 'pg-toggle-visibility) - (define-key map [(control mouse-3)] 'proof-mouse-goto-point) + (define-key map [(control meta mouse-3)] 'proof-mouse-goto-point) ;; NB: next binding overwrites comint-find-source-code. (define-key map [(meta p)] 'pg-previous-matching-input-from-input) (define-key map [(meta n)] 'pg-next-matching-input-from-input) |