diff options
| -rw-r--r-- | coq.el | 7 | ||||
| -rw-r--r-- | lego.el | 7 | ||||
| -rw-r--r-- | proof.el | 5 |
3 files changed, 11 insertions, 8 deletions
@@ -3,6 +3,9 @@ ;; Author: Healfdene Goguen and Thomas Kleymann ;; $Log$ +;; Revision 1.15 1998/03/25 17:30:35 tms +;; added support for etags at generic proof level +;; ;; Revision 1.14 1998/01/15 13:30:18 hhg ;; Added coq-shell-cd ;; Some new fontlocks @@ -561,10 +564,6 @@ (proof-config-done) -; (define-key (current-local-map) [(meta tab)] -; (if (fboundp 'complete-tag) -; 'complete-tag ; Emacs 19.31 (superior etags) -; 'tag-complete-symbol)) ;XEmacs 19.13 (inferior etags) (define-key (current-local-map) [(control c) (control p)] 'coq-prf) (define-key (current-local-map) [(control c) c] 'coq-ctxt) (define-key (current-local-map) [(control c) h] 'coq-help) @@ -5,6 +5,9 @@ ;; $Log$ +;; Revision 1.37 1998/03/25 17:30:41 tms +;; added support for etags at generic proof level +;; ;; Revision 1.36 1998/02/10 14:12:56 tms ;; added Dnf to lego-undoable-commands-regexp ;; @@ -599,10 +602,6 @@ (proof-config-done) - (define-key (current-local-map) [(meta tab)] - (if (fboundp 'complete-tag) - 'complete-tag ; Emacs 19.31 (superior etags) - 'tag-complete-symbol)) ;XEmacs 19.13 (inferior etags) (define-key (current-local-map) [(control c) (control p)] 'lego-prf) (define-key (current-local-map) [(control c) c] 'lego-ctxt) (define-key (current-local-map) [(control c) h] 'lego-help) @@ -9,6 +9,9 @@ ;; $Log$ +;; Revision 1.35 1998/03/25 17:30:28 tms +;; added support for etags at generic proof level +;; ;; Revision 1.34 1998/03/24 17:26:15 tms ;; *** empty log message *** ;; @@ -1478,6 +1481,8 @@ current command." ;; keymap + (define-key proof-mode-map [(meta tab)] 'tag-complete-symbol) + (define-key proof-mode-map (vconcat [(control c)] (vector proof-terminal-char)) 'proof-active-terminator-minor-mode) |