diff options
| -rw-r--r-- | generic/proof-script.el | 39 | ||||
| -rw-r--r-- | generic/proof-shell.el | 3 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 1 |
3 files changed, 31 insertions, 12 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index c8baac64..3b2125da 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1610,16 +1610,21 @@ No action if BUF is nil." ;; UGLY COMPATIBILITY FIXME: remove this soon (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) "--:doubleLine" "----")) - (list - ["Submit bug report" - proof-submit-bug-report - :active t]) - ;; UGLY COMPATIBILITY FIXME: remove this soon - (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) - "--:doubleLine" "----")) ) "Proof General menu for various modes.") +(defvar proof-bug-report-menu + (append + ;; UGLY COMPATIBILITY FIXME: remove this soon + (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) + "--:doubleLine" "----")) + (list + ["Submit bug report" + proof-submit-bug-report + :active t])) + "Proof General menu for submitting bug report (one item plus separator).") + + (defvar proof-menu (append '(["Active terminator" proof-active-terminator-minor-mode :active t @@ -1748,13 +1753,25 @@ Otherwise just do proof-restart-buffers to delete some spans from memory." (let ((map proof-mode-map)) (define-key map [(control c) (control e)] 'proof-find-next-terminator) (define-key map [(control c) (control a)] 'proof-goto-command-start) -(define-key map [(control c) (control n)] 'proof-assert-next-command-interactive) + +;; Sep'99. FIXME: key maps need reorganizing, so do the assert-until style +;; functions. I've re-bound C-c C-n and C-c C-u to the toolbar functions +;; to make the behaviour the same. People find the "enhanced" behaviour +;; of the other functions confusing. Moreover the optional argument +;; to delete is a bad thing for C-c C-u, since repeating it fast will +;; tend to delete! +(define-key map [(control c) (control n)] 'proof-toolbar-next) +(define-key map [(control c) (control u)] 'proof-toolbar-undo) +(define-key map [(control c) (control b)] 'proof-toolbar-use) +(define-key map [(control c) (control r)] 'proof-toolbar-retract) ;; new binding + +;;;; (define-key map [(control c) (control n)] 'proof-assert-next-command-interactive) ;; FIXME : This ought to be set to 'proof-assert-until point (define-key map [(control c) (return)] 'proof-assert-next-command-interactive) (define-key map [(control c) (control t)] 'proof-try-command) ;; FIXME: The following two functions should be unified. (define-key map [(control c) ?u] 'proof-retract-until-point-interactive) -(define-key map [(control c) (control u)] 'proof-undo-last-successful-command-interactive) +;;;; (define-key map [(control c) (control u)] 'proof-undo-last-successful-command-interactive) (define-key map [(control c) ?\'] 'proof-goto-end-of-locked-interactive) ;; FIXME da: I don't understand what this function is supposed to do. ;; It will copy a proof command from within the locked region @@ -1762,7 +1779,8 @@ Otherwise just do proof-restart-buffers to delete some spans from memory." ;; do with shell). Perhaps we could define a ;; collection of useful copying functions which do this kind of thing. ;; (define-key map [(control button1)] 'proof-send-span) -(define-key map [(control c) (control b)] 'proof-process-buffer) +;;; (define-key map [(control c) (control b)] 'proof-process-buffer) + (define-key map [(control c) (control z)] 'proof-frob-locked-end) (define-key map [(control c) (control p)] 'proof-prf) (define-key map [(control c) ?c] 'proof-ctxt) @@ -1843,6 +1861,7 @@ finish setup which depends on specific proof assistant configuration." "Internals")) nil) ;; end UGLY COMPATIBILTY HACK + proof-bug-report-menu ))) ;; Put the ProofGeneral menu on the menubar diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 6e9f7f0a..9f8d2458 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1608,8 +1608,7 @@ before and after sending the command." (easy-menu-define proof-response-mode-menu proof-response-mode-map "Menu for Proof General response buffer." - (cons proof-general-name - (cdr proof-shared-menu))) + (cons proof-general-name proof-shared-menu)) (provide 'proof-shell) diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index bea72456..27530c21 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -318,6 +318,7 @@ Move point if the end of the locked position is invisible." (defun proof-toolbar-retract-enable-p () (not (proof-locked-region-empty-p))) +;; FIXME: to become proof-retract-buffer (defun proof-toolbar-retract () "Retract entire buffer." ;; proof-retract-file might be better here! |