diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-06-08 20:51:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-06-08 20:51:50 +0000 |
| commit | 73cb28aac0f12b864338077a457b3347592ba345 (patch) | |
| tree | 0795078f1ac17ff4358666834a330e3048080290 /generic | |
| parent | 52bb9c18eed420f15139528c712641fb9886720d (diff) | |
GNU Emacs keybinding for pg-identifier-under-mouse-query
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index b30b2a03..56bd2970 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1032,9 +1032,13 @@ The function `substitute-command-keys' is called on the argument." ;; Identifier under mouse query (added in PG 3.5) ;; -;; FIXME: next setting perhaps a bit obnoxious, but this modifier -;; combination is currently unused. -(global-set-key '(control meta button1) 'pg-identifier-under-mouse-query) +;; FIXME: making the binding globally is perhaps a bit obnoxious, but +;; this modifier combination is currently unused. +(cond + (proof-running-on-Emacs21 + (global-set-key [C-M-mouse-1] 'pg-identifier-under-mouse-query)) + (proof-running-on-Xemacs + (global-set-key '(control meta button1) 'pg-identifier-under-mouse-query))) (defun pg-identifier-under-mouse-query (event) (interactive "e") |