diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2006-08-25 08:37:23 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2006-08-25 08:37:23 +0000 |
| commit | a82daf51268be086f3da32294d7e91170426cba7 (patch) | |
| tree | 53663099da87121c748eb02d56d8da95fbd71590 /coq/coq-abbrev.el | |
| parent | 11befe15a85ab4120bb251be9443d9c0834db3ef (diff) | |
Fixed a small bug in indentation of coq.
Fixed behavior for making abbrev table (don't if it already exists).
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index d8a53f47..164ac4a5 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -51,15 +51,18 @@ (coq-build-abbrev-table-from-db coq-terms-db)) + ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -(if (boundp 'holes-abbrev-complete) - () +(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))) + (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)) ;;;;; |