gitback/doomemacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lang/coq: setup company ourselves + minor refactor

Browse Source 
company-coq imposes its own value for company-idle-delay, potentially
overriding the user's customizations, so we set up company ourselves.
This commit is contained in:
Henrik Lissner 2019-10-21 08:46:40 -04:00
parent 573675b6e8
commit 8eb9cf5b30
No known key found for this signature in database
GPG Key ID: 5F6C0EA160557395
1 changed files with 17 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
modules/lang/coq/config.el
View File

@ -13,17 +13,14 @@
;;;###package coq
;; Doom syncs other indent variables with `tab-width'; we are trusting major
;; modes to set it -- which most of them do -- but coq-mode doesn't, so...
;; Doom syncs other indent variables with `tab-width'; we trust major modes to
;; set it -- which most of them do -- but coq-mode doesn't, so...
(setq-hook! 'coq-mode-hook tab-width proof-indent)
;; We've replaced coq-mode abbrevs with yasnippet snippets (in the snippets
;; library included with Doom).
(setq coq-mode-abbrev-table '())
(when (featurep! :completion company)
(add-hook 'coq-mode-hook #'company-coq-mode))
(map! :after coq-mode
:map coq-mode-map
:localleader
@ -65,14 +62,26 @@
"T" #'coq-insert-tactical))
(after! company-coq
;; This package provides more than just code completion, so we load it whether
;; or not :completion company is enabled.
(use-package! company-coq
:hook (coq-mode . company-coq-mode)
:config
(set-popup-rule! "^\\*\\(?:response\\|goals\\)\\*" :ignore t)
(set-lookup-handlers! 'company-coq-mode
:definition #'company-coq-jump-to-definition
:references #'company-coq-grep-symbol
:documentation #'company-coq-doc)
(unless (featurep! :completion company)
(setq company-coq-disabled-features '(company company-defaults)))
(if (not (featurep! :completion company))
(setq company-coq-disabled-features '(company company-defaults))
;; `company-coq''s company defaults impose idle-completion on folks, so
;; we'll set up company ourselves.
(add-to-list 'company-coq-disabled-features 'company-defaults)
;; See https://github.com/cpitclaudel/company-coq/issues/42
(map! :map coq-mode-map [remap company-complete-common]
#'company-indent-or-complete-common))
(map! :map coq-mode-map
:localleader
"ao" #'company-coq-occur