diff options
| -rw-r--r-- | generic/proof-config.el | 23 | ||||
| -rw-r--r-- | generic/proof-menu.el | 6 |
2 files changed, 17 insertions, 12 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index fe53f61a..01f72cc3 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -2620,15 +2620,20 @@ If this table is empty or needs adjusting, please make changes using (if proof-running-on-XEmacs '([(control c) \`] . proof-next-error) '("`" . proof-next-error)) - '(([(control c) (control c)] . proof-interrupt-process) - ([(control c) (control n)] . proof-assert-next-command-interactive) - ([(control c) (control u)] . proof-undo-last-successful-command) - ([(control c) (control p)] . proof-prf) - ([(control c) (control l)] . proof-layout-windows) - ([(control c) (control x)] . proof-shell-exit) - ([(control c) (control s)] . proof-shell-start) - ([(control c) (control v)] . proof-minibuffer-cmd) - ([(control c) (control w)] . pg-response-clear-displays))) + '(([(control c) (control c)] . proof-interrupt-process) + ([(control c) (control n)] . proof-assert-next-command-interactive) + ([(control c) (control u)] . proof-undo-last-successful-command) + ([(control c) (control p)] . proof-prf) + ([(control c) (control l)] . proof-layout-windows) + ([(control c) (control x)] . proof-shell-exit) + ([(control c) (control s)] . proof-shell-start) + ([(control c) (control v)] . proof-minibuffer-cmd) + ([(control c) (control w)] . pg-response-clear-displays) + ;; PG 3.6: Some more key bindings moved here from script mode, + ;; users suggest they ought to work in other PG buffers too. + ([(control c) (control ?.)] . proof-goto-end-of-locked) + ([(control c) (control f)] . proof-find-theorems) + ([(control c) (control o)] . proof-display-some-buffers))) "List of key-bindings made for the script, goals and response buffer. Elements of the list are tuples `(k . f)' where `k' is a key-binding (vector) and `f' the designated function." diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 56ce5208..03da8467 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -89,11 +89,11 @@ without adjusting window layout." (define-key map [(control c) (control a)] (proof-ass keymap)) (define-key map [(control c) (control b)] 'proof-process-buffer) ;; C-c C-c is proof-interrupt-process in universal-keys -(define-key map [(control c) (control f)] 'proof-find-theorems) +;; C-c C-f is proof-find-theorems in universal-keys (define-key map [(control c) (control h)] 'proof-help) ;; C-c C-l is proof-layout-windows in universal-keys ;; C-c C-n is proof-assert-next-command-interactive in universal-keys -(define-key map [(control c) (control o)] 'proof-display-some-buffers) +;; C-c C-o is proof-display-some-buffers in universal-keys (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) @@ -103,7 +103,7 @@ without adjusting window layout." (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 ?.)] 'proof-goto-end-of-locked) +; C-c C-. is proof-goto-end-of-locked in universal-keys (define-key map [(control c) (control return)] 'proof-goto-point) (define-key map [(control c) v] 'pg-toggle-visibility);; FIXME: FSF?? (cond ((string-match "XEmacs" emacs-version) |