emenel/doomemacs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

lang/coq: general refactor

Browse source 
Potentially fixes #1854
This commit is contained in:
Henrik Lissner 2019-10-04 15:33:37 -04:00
parent f6a182d69c
commit c21607ae66
No known key found for this signature in database
GPG key ID: 5F6C0EA160557395
2 changed files with 19 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

15
modules/lang/coq/autoload.el
View file

@ -1,15 +0,0 @@
;;; lang/coq/autoload.el -*- lexical-binding: t; -*-
;; HACK `proof-general' ascertains its own library path at compile time in its
;; autoloads file using `byte-compile-current-file' (and stores it in
;; `pg-init--script-full-path'). This means that when
;; `doom-package-autoload-file' is created and byte-compiled,
;; `pg-init--script-full-path' will be wrong, causing file-missing errors as it
;; tries to load `proof-site'. We prevent this by defining these two variables
;; early, in our own autoloads file.
;;;###autoload
(setq pg-init--script-full-path (locate-library "proof-general")
pg-init--pg-root (file-name-directory pg-init--script-full-path))
;;;###autoload
(add-hook 'coq-mode-hook #'company-coq-mode)

23
modules/lang/coq/config.el
View file

@ -1,12 +1,27 @@
;;; lang/coq/config.el -*- lexical-binding: t; -*-
;; `coq'
;;;###package proof-general
;; HACK `proof-general' ascertains its own library path at compile time in its
;; autoloads file using `byte-compile-current-file' (and stores it in
;; `pg-init--script-full-path'). This means that when
;; `doom-package-autoload-file' is created and byte-compiled,
;; `pg-init--script-full-path' will be wrong, causing file-missing errors as it
;; 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))
;;;###package coq
(setq proof-electric-terminator-enable t)
;; 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
@ -47,6 +62,7 @@
"t" #'coq-insert-tactic
"T" #'coq-insert-tactical))
(after! company-coq
(set-popup-rule! "^\\*\\(?:response\\|goals\\)\\*" :ignore t)
(set-lookup-handlers! 'company-coq-mode
@ -55,13 +71,12 @@
:documentation #'company-coq-doc)
(unless (featurep! :completion company)
(setq company-coq-disabled-features '(company company-defaults)))
(map! :map coq-mode-map
:localleader
(:prefix ("i" . "insert")
"ao" #'company-coq-occur
(:prefix "i"
"l" #'company-coq-lemma-from-goal
"m" #'company-coq-insert-match-construct)
"ao" #'company-coq-occur
(:prefix ("h" . "help")
"e" #'company-coq-document-error
"E" #'company-coq-browse-error-messages