From d9f819dac4ec4e8d0b707717dd734098e569d838 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 27 Aug 2018 12:57:07 +0200 Subject: [PATCH 1/6] Only make company features conditional --- modules/lang/coq/autoload.el | 1 - modules/lang/coq/config.el | 5 +++++ modules/lang/coq/packages.el | 3 +-- 3 files changed, 6 insertions(+), 3 deletions(-) create mode 100644 modules/lang/coq/config.el diff --git a/modules/lang/coq/autoload.el b/modules/lang/coq/autoload.el index 390a3f94f..624185018 100644 --- a/modules/lang/coq/autoload.el +++ b/modules/lang/coq/autoload.el @@ -1,5 +1,4 @@ ;;; lang/coq/autoload.el -*- lexical-binding: t; -*- -;;;###if (featurep! :completion company) ;;;###autoload (add-hook 'coq-mode-hook #'company-coq-mode) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el new file mode 100644 index 000000000..eeb919779 --- /dev/null +++ b/modules/lang/coq/config.el @@ -0,0 +1,5 @@ +;;; lang/coq/config.el -*- lexical-binding: t; -*- + +(after! company-coq + (when (not (featurep! :completion company)) + (setq company-coq-disabled-features '(company company-defaults)))) diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el index 69d5299b5..3ae652118 100644 --- a/modules/lang/coq/packages.el +++ b/modules/lang/coq/packages.el @@ -3,5 +3,4 @@ (package! proof-general :recipe (:fetcher github :repo "ProofGeneral/PG" :files ("*"))) -(when (featurep! :completion company) - (package! company-coq)) +(package! company-coq) From 5492315053fdc0957ed4e60e096551039c11a395 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 27 Aug 2018 13:57:00 +0200 Subject: [PATCH 2/6] Added lookup handlers --- modules/lang/coq/config.el | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index eeb919779..b91cb9efb 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -1,5 +1,9 @@ ;;; lang/coq/config.el -*- lexical-binding: t; -*- (after! company-coq + (set-lookup-handlers! 'company-coq-mode + :definition #'company-coq-jump-to-definition + :references #'company-coq-occur + :documentation #'company-coq-doc) (when (not (featurep! :completion company)) (setq company-coq-disabled-features '(company company-defaults)))) From f6e9b943fd673213646d7ff9bcddc1d12b1561e7 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 27 Aug 2018 14:11:14 +0200 Subject: [PATCH 3/6] Change ref function --- modules/lang/coq/config.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index b91cb9efb..2997369b8 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -3,7 +3,7 @@ (after! company-coq (set-lookup-handlers! 'company-coq-mode :definition #'company-coq-jump-to-definition - :references #'company-coq-occur + :references #'company-coq-grep-symbol :documentation #'company-coq-doc) (when (not (featurep! :completion company)) (setq company-coq-disabled-features '(company company-defaults)))) From 953906ccdb62e904431c67992294a9429b364ca0 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Mon, 27 Aug 2018 15:35:18 +0200 Subject: [PATCH 4/6] Terminator triggers evaluation --- modules/lang/coq/config.el | 3 +++ 1 file changed, 3 insertions(+) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 2997369b8..518c08d9d 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -1,5 +1,8 @@ ;;; lang/coq/config.el -*- lexical-binding: t; -*- +(after! coq + (setq proof-electric-terminator-enable t)) + (after! company-coq (set-lookup-handlers! 'company-coq-mode :definition #'company-coq-jump-to-definition From f95623989d515fae7295f9b1ca422477adea915c Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Fri, 31 Aug 2018 03:31:58 +0200 Subject: [PATCH 5/6] lang/coq: remove unnecessary after! For setting a variable, an after! block is overkill --- modules/lang/coq/config.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 518c08d9d..fc2b0b85e 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -1,7 +1,7 @@ ;;; lang/coq/config.el -*- lexical-binding: t; -*- -(after! coq - (setq proof-electric-terminator-enable t)) +;; `coq' +(setq proof-electric-terminator-enable t) (after! company-coq (set-lookup-handlers! 'company-coq-mode From f75381ae51e40cbd4fdb8e14e4e414b8f6db8ef9 Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Fri, 31 Aug 2018 03:32:25 +0200 Subject: [PATCH 6/6] when not => unless --- modules/lang/coq/config.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index fc2b0b85e..1ff5cc560 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -8,5 +8,5 @@ :definition #'company-coq-jump-to-definition :references #'company-coq-grep-symbol :documentation #'company-coq-doc) - (when (not (featurep! :completion company)) + (unless (featurep! :completion company) (setq company-coq-disabled-features '(company company-defaults))))