diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2008-01-17 12:15:18 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-17 12:15:18 +0000 |
commit | 42031b5275f51bbaa5a84d1a0c98a3072bd03553 (patch) | |
tree | 9ca0d3d0b8709d65f88c3a3a3395386d18dfb73d /generic/proof-menu.el | |
parent | d7df9ffe5191aab4f54938fcf63fcd144a123722 (diff) |
Remove dummy defvars, which cause errors if proof-menu is required during compile. Add keybindings for history. Move About menu item.
Diffstat (limited to 'generic/proof-menu.el')
-rw-r--r-- | generic/proof-menu.el | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 75068e41..0d4133ec 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -7,10 +7,6 @@ ;; $Id$ ;; -(eval-when-compile - (defvar proof-mode-map nil) - (defvar proof-assistant-menu nil)) ; avoid compile warnings - (require 'proof) ; proof-deftoggle, proof-eval-when-ready-for-assistant ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -80,6 +76,7 @@ without adjusting window layout." ;;;###autoload (defun proof-menu-define-keys (map) + ;; Prover specific keymap under C-c C-a (proof-eval-when-ready-for-assistant (define-key map [(control c) (control a)] (proof-ass keymap))) ;; M-a and M-e are usually {forward,backward}-sentence. @@ -116,9 +113,8 @@ without adjusting window layout." (t (define-key map [(control mouse-3)] 'proof-mouse-goto-point))) ;; NB: next binding overwrites comint-find-source-code. - ;; TODO: not implemented yet - ;; (define-key map [(meta p)] 'proof-previous-matching-command) - ;; (define-key map [(meta n)] 'proof-next-matching-command) + (define-key map [(meta p)] 'pg-previous-matching-input-from-input) + (define-key map [(meta n)] 'pg-next-matching-input-from-input) ;; Standard binding for completion (define-key map [(control return)] 'proof-script-complete) (define-key map [(control c) (control ?\;)] 'pg-insert-last-output-as-comment) @@ -211,9 +207,9 @@ without adjusting window layout." (defvar proof-help-menu '("Help" + ["About PG" proof-splash-display-screen t] ["PG Info" (info "ProofGeneral") t] ["PG Homepage" (browse-url proof-general-home-page) t] - ["About PG" proof-splash-display-screen t] ["Send Bug Report" proof-submit-bug-report t]) "Proof General help menu.") |