diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2008-01-03 19:46:45 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2008-01-03 19:46:45 +0000 |
| commit | a06c46188f73f488b0ac860d30e9e9037468543b (patch) | |
| tree | 68dfb7c5f298921405542d4cdc91850318c5886c /coq/coq-abbrev.el | |
| parent | cd51d90608b090a030a26883035888d673b935d9 (diff) | |
Fixed abbrev installation. + small fixes.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index c91911fb..b6ad7b51 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -19,14 +19,13 @@ (defconst coq-tactics-menu (append '("INSERT TACTICS" ["Intros (smart)" coq-insert-intros t]) - (coq-build-menu-from-db coq-tactics-db))) + (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db)))) (defconst coq-tactics-abbrev-table - (coq-build-abbrev-table-from-db coq-tactics-db)) + (coq-build-abbrev-table-from-db (append coq-tactics-db coq-solve-tactics-db))) (defconst coq-tacticals-menu - (append '("INSERT TACTICALS" - ["Intros (smart)" coq-insert-intros t]) + (append '("INSERT TACTICALS") (coq-build-menu-from-db coq-tacticals-db))) (defconst coq-tacticals-abbrev-table @@ -54,17 +53,21 @@ ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -;; (unless (noninteractive) -;; (if (and (boundp 'coq-mode-abbrev-table) -;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) -;; (message "Coq abbrevs already exists, default not loaded") -;; (message "Coq default abbrevs loaded") -;; (define-abbrev-table 'coq-mode-abbrev-table -;; (append coq-tactics-abbrev-table coq-tacticals-abbrev-table -;; coq-commands-abbrev-table coq-terms-abbrev-table)) -;; ;; if we use default coq abbrev, never ask to save it -;; (setq save-abbrevs nil))) - +(defun coq-install-abbrevs () + "install default abbrev table for coq if no other already is." + (if (and (boundp 'coq-mode-abbrev-table) + (not (equal coq-mode-abbrev-table (make-abbrev-table)))) + (message "Coq abbrevs already exists, default not loaded") + (define-abbrev-table 'coq-mode-abbrev-table + (append coq-tactics-abbrev-table coq-tacticals-abbrev-table + coq-commands-abbrev-table coq-terms-abbrev-table)) + ;; if we use default coq abbrev, never ask to save it + (setq save-abbrevs nil) + (message "Coq default abbrevs loaded") + )) + +(unless (noninteractive) + (coq-install-abbrevs)) ;;;;; ;; The coq menu mainly built from tables |