diff options
| author |  Stefan Monnier <monnier@iro.umontreal.ca> | 2011-06-07 01:47:24 +0000 |
|---|---|---|
| committer | Stefan Monnier <monnier@iro.umontreal.ca> | 2011-06-07 01:47:24 +0000 |
| commit | 34da1bb2cff1cf0f80ec6465c58f0680c3bb8d48 (patch) | |
| tree | b3d212d56f85c755414083f22006ee8515c93745 /coq/coq-abbrev.el | |
| parent | 56304ed772024e40fdf767fb8c3d1b3bc5e9ff27 (diff) | |
Summary: coq-smie: improve indentation.
* coq.el (coq-smie-grammar): Add rules for {|...|}, Let, Record, Module..End,
Section..End, and BeginSubproof..EndSubproof.
(coq-smie-search-token): New function.
(coq-smie-forward-token, coq-smie-backward-token): Recognize {| and |}.
Distinguish Module definition from Module introduction.
Merge "Module Type" and "Module".
(coq-smie-rules): Refine list-intro. Improve indentation after "with".
Add Function, Let and Record to the := case.
Indent within Module..End and friends. Improve indentation of record def.
Indent forall's body by 2. Better indent Lemmas.
* coq-db.el (coq-build-abbrev-table-from-db): Mark those abbrevs as `system'.
* coq-abbrev.el (coq-install-abbrevs): Don't bind save-abbrevs
since it's not needed any more.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 3c926639..538ad5ec 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -61,12 +61,9 @@ ;; da: this test will always fail. Assume bound-->non-empty ;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) (message "Coq abbrevs already exists, default not loaded") - (let - ;; prevent query to immediately save these abbrevs - ((save-abbrevs nil)) - (define-abbrev-table 'coq-mode-abbrev-table - (append coq-tactics-abbrev-table coq-tacticals-abbrev-table - coq-commands-abbrev-table coq-terms-abbrev-table))) + (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 ;; PC: fix trac #382 I comment this. But how to disable abbrev ;; saving for coq mode only? |