8f1a5d6fd5
- delete some diminish expressions which are not related to PG and user spacemacs|hide-lighter instead of spacemacs|diminish - move company related configuration to the correct place - move setq expressions to :init blocks to allow users to easily change them
110 lines
3.7 KiB
EmacsLisp
110 lines
3.7 KiB
EmacsLisp
;;; packages.el --- coq layer packages file for Spacemacs.
|
|
;;
|
|
;; Copyright (c) 2012-2016 Sylvain Benner & Contributors
|
|
;;
|
|
;; Author: Jeremy Bi <bixuanxbi@gmail.com>
|
|
;; URL: https://github.com/syl20bnr/spacemacs
|
|
;;
|
|
;; This file is not part of GNU Emacs.
|
|
;;
|
|
;;; License: GPLv3
|
|
|
|
(setq coq-packages
|
|
'(
|
|
(company-coq :toggle (configuration-layer/package-usedp 'company))
|
|
(proof-general :location (recipe
|
|
:fetcher github
|
|
:repo "ProofGeneral/PG"
|
|
:files ("*")))
|
|
smartparens
|
|
vi-tilde-fringe
|
|
))
|
|
|
|
(defun coq/init-company-coq ()
|
|
(use-package company-coq
|
|
:defer t
|
|
:init
|
|
(progn
|
|
(add-hook 'coq-mode-hook #'company-coq-mode)
|
|
(add-to-list 'spacemacs-jump-handlers-coq-mode
|
|
'company-coq-jump-to-definition)
|
|
(setq company-coq-disabled-features '(hello)))
|
|
:config
|
|
(progn
|
|
(spacemacs|hide-lighter company-coq-mode)
|
|
(spacemacs/declare-prefix-for-mode 'coq-mode
|
|
"mi" "coq/insert")
|
|
(spacemacs/set-leader-keys-for-major-mode 'coq-mode
|
|
"il" 'company-coq-lemma-from-goal
|
|
"im" 'company-coq-insert-match-construct
|
|
"ao" 'company-coq-occur))))
|
|
|
|
(defun coq/init-proof-general ()
|
|
(use-package proof-site
|
|
:mode ("\\.v\\'" . coq-mode)
|
|
:defer t
|
|
:init
|
|
(progn
|
|
(setq coq/proof-general-load-path
|
|
(concat (configuration-layer/get-elpa-package-install-directory
|
|
'proof-general) "generic")
|
|
proof-three-window-mode-policy 'hybrid
|
|
proof-script-fly-past-comments t
|
|
proof-splash-seen t)
|
|
(add-to-list 'load-path coq/proof-general-load-path))
|
|
:config
|
|
(progn
|
|
(spacemacs|hide-lighter holes-mode)
|
|
(spacemacs|hide-lighter proof-active-buffer-fake-minor-mode)
|
|
;; key bindings
|
|
(dolist (prefix '(("ml" . "pg/layout")
|
|
("mp" . "pg/prover")
|
|
("ma" . "pg/ask-prover")
|
|
("mai" . "show-implicits")
|
|
("mg" . "pg/goto")))
|
|
(spacemacs/declare-prefix-for-mode
|
|
'coq-mode
|
|
(car prefix) (cdr prefix)))
|
|
(spacemacs/set-leader-keys-for-major-mode 'coq-mode
|
|
;; Basic proof management
|
|
"]" 'proof-assert-next-command-interactive
|
|
"[" 'proof-undo-last-successful-command
|
|
"." 'proof-goto-point
|
|
;; Layout
|
|
"lc" 'pg-response-clear-displays
|
|
"ll" 'proof-layout-windows
|
|
"lp" 'proof-prf
|
|
;; Prover Interaction
|
|
"pi" 'proof-interrupt-process
|
|
"pp" 'proof-process-buffer
|
|
"pq" 'proof-shell-exit
|
|
"pr" 'proof-retract-buffer
|
|
;; Prover queries ('ask prover')
|
|
"aa" 'coq-Print
|
|
"aA" 'coq-Print-with-all
|
|
"ab" 'coq-About
|
|
"aB" 'coq-About-with-all
|
|
"ac" 'coq-Check
|
|
"aC" 'coq-Check-show-all
|
|
"af" 'proof-find-theorems
|
|
"aib" 'coq-About-with-implicits
|
|
"aic" 'coq-Check-show-implicits
|
|
"aii" 'coq-Print-with-implicits
|
|
;; Moving the point (goto)
|
|
"ge" 'proof-goto-command-end
|
|
"gl" 'proof-goto-end-of-locked
|
|
"gs" 'proof-goto-command-start
|
|
;; Insertions
|
|
"ie" 'coq-end-Section))))
|
|
|
|
(defun coq/post-init-smartparens ()
|
|
(spacemacs/add-to-hooks (if dotspacemacs-smartparens-strict-mode
|
|
'smartparens-strict-mode
|
|
'smartparens-mode)
|
|
'(coq-mode-hook)))
|
|
|
|
(defun coq/post-init-vi-tilde-fringe ()
|
|
(spacemacs/add-to-hooks 'spacemacs/disable-vi-tilde-fringe
|
|
'(coq-response-mode-hook
|
|
coq-goals-mode-hook)))
|