mirror of
https://gitlab.com/dwt1/dotfiles.git
synced 2026-04-24 03:50:24 +10:00
Updating Doom Emacs.
This commit is contained in:
@@ -1,22 +1,17 @@
|
||||
;;; lang/coq/config.el -*- lexical-binding: t; -*-
|
||||
|
||||
;;;###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)
|
||||
proof-splash-enable nil)
|
||||
(setq proof-splash-enable nil)
|
||||
|
||||
|
||||
;;;###package coq
|
||||
;; 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)
|
||||
(setq-hook! 'coq-mode-hook
|
||||
;; 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...
|
||||
tab-width proof-indent
|
||||
;; HACK Fix #2081: Doom continues comments on RET, but coq-mode doesn't have a
|
||||
;; sane `comment-line-break-function', so...
|
||||
comment-line-break-function nil)
|
||||
|
||||
;; We've replaced coq-mode abbrevs with yasnippet snippets (in the snippets
|
||||
;; library included with Doom).
|
||||
@@ -77,11 +72,11 @@
|
||||
(setq company-coq-disabled-features '(hello company-defaults))
|
||||
|
||||
(if (featurep! :completion company)
|
||||
(map! :map coq-mode-map [remap company-complete-common]
|
||||
#'company-indent-or-complete-common)
|
||||
(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
|
||||
;; we'll set up company ourselves. See
|
||||
;; https://github.com/cpitclaudel/company-coq/issues/42
|
||||
(add-to-list 'company-coq-disabled-features 'company))
|
||||
|
||||
(map! :map coq-mode-map
|
||||
|
||||
@@ -1,6 +1,5 @@
|
||||
;; -*- no-byte-compile: t; -*-
|
||||
;;; lang/coq/packages.el
|
||||
|
||||
(package! proof-general)
|
||||
|
||||
(package! company-coq)
|
||||
(package! proof-general :pin "9196749d55")
|
||||
(package! company-coq :pin "f9dba9ddff")
|
||||
|
||||
Reference in New Issue
Block a user