From 5738e39fea05e4f9cfe5f7783c6be1b9184fceab Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sun, 17 Nov 2019 00:33:52 +0900 Subject: [PATCH 1/4] Disable proof general's splash screen --- modules/lang/coq/config.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 086d3648b..ef7ef196f 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -9,7 +9,8 @@ ;; tries to load `proof-site'. We prevent this by defining these two variables ;; early, in our own autoloads file. (setq pg-init--script-full-path (locate-library "proof-general") - pg-init--pg-root (file-name-directory pg-init--script-full-path)) + pg-init--pg-root (file-name-directory pg-init--script-full-path) + proof-splash-enable nil) ;;;###package coq From 78bb2e2ae54d9e1b711212af1bda34e4eb0624bb Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sun, 17 Nov 2019 00:34:15 +0900 Subject: [PATCH 2/4] diable the hello feature of company-coq --- modules/lang/coq/config.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index ef7ef196f..2383e8be7 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -75,10 +75,11 @@ :documentation #'company-coq-doc) (if (not (featurep! :completion company)) - (setq company-coq-disabled-features '(company company-defaults)) + (setq company-coq-disabled-features '(hello 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) + (add-to-list 'company-coq-disabled-features 'hello) ;; See https://github.com/cpitclaudel/company-coq/issues/42 (map! :map coq-mode-map [remap company-complete-common] #'company-indent-or-complete-common)) From c4fad17c2914362fc0de576bcd4589a521dbe0d7 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sun, 17 Nov 2019 01:21:11 +0900 Subject: [PATCH 3/4] Remove company-coq's hello page --- modules/lang/coq/config.el | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 2383e8be7..757c376a6 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -74,12 +74,12 @@ :references #'company-coq-grep-symbol :documentation #'company-coq-doc) + (setq company-coq-disabled-features '(hello company-defaults)) + (if (not (featurep! :completion company)) - (setq company-coq-disabled-features '(hello company company-defaults)) + (add-to-list 'company-coq-disabled-features 'company) ;; `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) - (add-to-list 'company-coq-disabled-features 'hello) ;; See https://github.com/cpitclaudel/company-coq/issues/42 (map! :map coq-mode-map [remap company-complete-common] #'company-indent-or-complete-common)) From a4e9d85db4e1dccce3cf161487f1a47626a5b02c Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sun, 17 Nov 2019 01:22:12 +0900 Subject: [PATCH 4/4] invert (if (not ..)) statement --- modules/lang/coq/config.el | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 757c376a6..86cd6ee0b 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -76,13 +76,13 @@ (setq company-coq-disabled-features '(hello company-defaults)) - (if (not (featurep! :completion company)) - (add-to-list 'company-coq-disabled-features 'company) + (if (featurep! :completion company) + (map! :map 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 - (map! :map coq-mode-map [remap company-complete-common] - #'company-indent-or-complete-common)) + (add-to-list 'company-coq-disabled-features 'company)) (map! :map coq-mode-map :localleader