diff options
author | 2000-06-05 13:52:06 +0000 | |
---|---|---|
committer | 2000-06-05 13:52:06 +0000 | |
commit | e1b23bfc50feb02a18c7a2ebad5637cf931a3949 (patch) | |
tree | 66affbe55a08be15f4cd324370ffc1a6df121833 | |
parent | 47fef0c2fd5b0a8e09ef5d4b4508347b4828dd3c (diff) |
Added miscellaneous commands section, with proof-display-some-buffers
function.
Bind C-c C-l to proof-display-some-buffers, add to buffer menu.
Move start/exit to proof assistant specific menu.
Added proof-next-error to menu.
-rw-r--r-- | generic/proof-menu.el | 64 |
1 files changed, 42 insertions, 22 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 0821b4fa..69a2fcc1 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -1,4 +1,4 @@ -;; proof-menu.el Menu and keymaps for Proof General +;; proof-menu.el Menus, keymaps, and misc commands for Proof General ;; ;; Copyright (C) 2000 LFCS Edinburgh. ;; Authors: David Aspinall @@ -11,6 +11,21 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; +;;; Miscellaneous commands +;;; + +(defun proof-display-some-buffers () + "Display the reponse buffer, and maybe also the goals buffer. +If in three window or multiple frame mode, the goals buffer +is also displayed." + (interactive) + (proof-switch-to-buffer proof-response-buffer 'noselect) + (if (or proof-dont-switch-windows proof-multiple-frames-enable) + (proof-switch-to-buffer proof-goals-buffer 'noselect))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; ;;; Key bindings ;;; @@ -22,16 +37,19 @@ ;; (define-key map [(control c) (control e)] 'proof-goto-command-end) ;; (define-key map [(control c) (control a)] 'proof-goto-command-start) (define-key map [(control c) (control b)] 'proof-process-buffer) -; C-c C-c is proof-interrupt-process in universal-keys +;; C-c C-c is proof-interrupt-process in universal-keys +(define-key map [(control c) (control f)] 'proof-find-theorems) +(define-key map [(control c) (control h)] 'proof-help) +(define-key map [(control c) (control l)] 'proof-display-some-buffers) (define-key map [(control c) (control n)] 'proof-assert-next-command-interactive) (define-key map [(control c) (control p)] 'proof-prf) (define-key map [(control c) (control r)] 'proof-retract-buffer) (define-key map [(control c) (control s)] 'proof-toggle-active-scripting) (define-key map [(control c) (control t)] 'proof-ctxt) (define-key map [(control c) (control u)] 'proof-undo-last-successful-command) +(define-key map [(control c) (control z)] 'proof-frob-locked-end) (define-key map [(control c) (control backspace)] 'proof-undo-and-delete-last-successful-command) ; C-c C-v is proof-minibuffer-cmd in universal-keys -(define-key map [(control c) (control z)] 'proof-frob-locked-end) (define-key map [(control c) (control ?.)] 'proof-goto-end-of-locked) (define-key map [(control c) (control return)] 'proof-goto-point) (cond ((string-match "XEmacs" emacs-version) @@ -40,15 +58,13 @@ (t (define-key map [mouse-3] 'proof-mouse-goto-point))) ; FSF ;; NB: next binding overwrites comint-find-source-code. -(define-key map [(control c) (control f)] 'proof-find-theorems) -(define-key map [(control c) (control h)] 'proof-help) ;; FIXME: not implemented yet ;; (define-key map [(meta p)] 'proof-previous-matching-command) ;; (define-key map [(meta n)] 'proof-next-matching-command) ;; Standard binding for completion (define-key map [(control return)] 'proof-script-complete) -;(define-key map [(control c) ?u] 'proof-retract-until-point-interactive) ;; Add the universal keys bound in all PG buffers. +;; C-c ` is next-error in universal-keys (proof-define-keys map proof-universal-keys)) @@ -100,6 +116,16 @@ (proof-menu-define-settings-menu)) '("----") (list + (vector + (concat "Start " proof-assistant) + 'proof-shell-start + ':active '(not (proof-shell-live-buffer))) + (vector + (concat "Exit " proof-assistant) + 'proof-shell-exit + ':active '(proof-shell-live-buffer))) + '("----") + (list (cons "Help" (append `(;; FIXME: should only put these two on the @@ -126,6 +152,10 @@ (defvar proof-buffer-menu '("Buffers" + ["Display some" + proof-display-some-buffers + :active (or (buffer-live-p proof-goals-buffer) + (buffer-live-p proof-response-buffer))] ["Active scripting" (proof-switch-to-buffer proof-script-buffer) :active (buffer-live-p proof-script-buffer)] @@ -150,7 +180,7 @@ (defvar proof-quick-opts-menu `("Options" - ["Don't switch windows" proof-dont-switch-windows-toggle + ["Three window mode" proof-dont-switch-windows-toggle :style toggle :selected proof-dont-switch-windows] ["Delete empty windows" proof-delete-empty-windows-toggle @@ -190,21 +220,9 @@ (defvar proof-shared-menu (append - ;; FIXME: should we move the start and stop items to - ;; the specific menu? - ;; (They only seem specific because they mention the PA). - (list - (vector - (concat "Start " proof-assistant) - 'proof-shell-start - ':active '(not (proof-shell-live-buffer))) - (vector - (concat "Exit " proof-assistant) - 'proof-shell-exit - ':active '(proof-shell-live-buffer))) - (list proof-buffer-menu) - (list proof-quick-opts-menu) - (list proof-help-menu)) + (list proof-buffer-menu) + (list proof-quick-opts-menu) + (list proof-help-menu)) "Proof General menu for various modes.") (defvar proof-bug-report-menu @@ -224,6 +242,8 @@ ["Function menu" function-menu :active (fboundp 'function-menu)] ["Complete identifier" complete t] + ["Next error" proof-next-error + :active proof-shell-next-error-regexp] "----") proof-shared-menu) "The Proof General generic menu.") |