aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-db.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2009-08-31 13:12:43 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2009-08-31 13:12:43 +0000
commitcb5d6b878af33521cfde310e00d882f42a66280a (patch)
tree113186a4b6b023d8b3bba810bcaf7ada37dd973c /coq/coq-db.el
parentab6cb06071add3dd02078d5d6199fadc171f0128 (diff)
Made customizable holes mode completion in abbreviations.
Diffstat (limited to 'coq/coq-db.el')
-rw-r--r--coq/coq-db.el12
1 files changed, 10 insertions, 2 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 4a62c30f..bcc4a1e4 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -189,6 +189,12 @@ structure."
(setq lgth (length l)))
res))
+(defcustom coq-holes-minor-mode t
+ "*Whether to apply holes minor mode (see `holes-show-doc') in
+ coq mode."
+ :type 'boolean
+ :group 'coq)
+
(defun coq-build-abbrev-table-from-db (db)
"Take a keyword database DB and return an abbrev table.
See `coq-syntax-db' for DB structure."
@@ -200,8 +206,10 @@ See `coq-syntax-db' for DB structure."
(e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
)
;; careful: nconc destructive!
- (when e2
- (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete)))))
+ (when e2
+ (if coq-holes-minor-mode
+ (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))
+ (setq res (nconc res (list `(,e2 ,e3))))))
(setq l tl)))
res))