aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-17 17:10:22 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-17 17:10:22 +0000
commit2abb0e6736c8681b1bb7eacdc4b14be13a36901d (patch)
tree7ff1ee365af68b2d07bc428c7077558359287ca0 /generic
parent31bf863ebbf5a71c1e03f01d3ed218a41a055a4a (diff)
Bind mouse 2 as well as mouse 3 for pbp
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-shell.el10
1 files changed, 6 insertions, 4 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7d232a5e..98ce3334 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1912,15 +1912,17 @@ May enable proof-by-pointing or similar features.
<<pbp-mode-map>>"
;; defined-derived-mode pbp-mode initialises pbp-mode-map
(setq proof-buffer-type 'pbp)
-; button 2 is a nuisance on 2 button mice
-; (define-key pbp-mode-map [(button2)] 'pbp-button-action)
- (define-key pbp-mode-map [mouse-3] 'pbp-button-action)
(cond
((string-match "XEmacs" emacs-version)
-
+ (define-key pbp-mode-map [(button2)] 'pbp-button-action)
+ (define-key pbp-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
+;; button 2 is a nuisance on 2 button mice, so we'll do 3 as well.
(define-key pbp-mode-map [(button3)] 'pbp-button-action)
(define-key pbp-mode-map [(control button3)] 'proof-undo-and-delete-last-successful-command))
(t
+ (define-key pbp-mode-map [mouse-2] 'pbp-button-action)
+ (define-key pbp-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
+ (define-key pbp-mode-map [mouse-3] 'pbp-button-action)
(define-key pbp-mode-map [C-mouse-3] 'proof-undo-and-delete-last-successful-command)))
(define-key pbp-mode-map [q] 'bury-buffer)
(easy-menu-add proof-goals-mode-menu pbp-mode-map)