From 61f69ca980a0f5009b65a0c0ae31db118c77301e Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Thu, 24 Apr 2025 18:58:02 -0400 Subject: [PATCH] fix(coq): corfu integration Makes company-coq cooperate wtih Corfu without activating company-mode. Needs more testing. --- modules/lang/coq/config.el | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 7fad2fd42..6bfe5195a 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -79,13 +79,25 @@ (setq company-coq-disabled-features '(hello company-defaults spinner)) - (if (modulep! :completion company) - (define-key coq-mode-map [remap company-complete-common] - #'company-indent-or-complete-common) - ;; `company-coq''s company defaults impose idle-completion on folks, so - ;; we'll set up company ourselves. See - ;; https://github.com/cpitclaudel/company-coq/issues/42 - (add-to-list 'company-coq-disabled-features 'company)) + (cond ((modulep! :completion corfu) + ;; HACK: company-coq activates `company-mode', though it's not really + ;; needed when we're relying on Corfu, hence these hacks: + (add-hook! 'coq-mode-local-vars-hook + (defun +coq-init-capf-completion-h () + (when (bound-and-true-p company-mode) + (company-mode -1)) + (add-hook 'completion-at-point-functions + (cape-company-to-capf 'company-coq) + nil t))) + (defadvice! +coq--proof-goto-point-advice (&rest _) + :override #'company-coq--proof-goto-point-advice + (when (bound-and-true-p company-candidates) + (company-abort)))) + + ;; DEPRECATED: The company module is deprecated. + ((modulep! :completion company) + (define-key coq-mode-map [remap company-complete-common] + #'company-indent-or-complete-common))) ;; HACK: Doom treats the use of package.el and its API as user error unless ;; they've called `package-initialize' themselves (in which case, it is