diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 9546a0199..086d3648b 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -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