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

Add coq key bindings

Browse source 
These bindings are modelled afer the bindings in spacemacs

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
This commit is contained in:
Rudi Grinberg 2019-09-07 17:00:23 +09:00
parent b6b2d74f25
commit 081e57dc10
1 changed files with 51 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -7,6 +7,45 @@
;; library included with Doom).
(setq coq-mode-abbrev-table '())
(map! :after coq-mode
:map coq-mode-map
:localleader
"]" #'proof-assert-next-command-interactive
"[" #'proof-undo-last-successful-command
"." #'proof-goto-point
(:prefix ("l" . "layout")
"c" #'pg-response-clear-displays
"l" #'proof-layout-windows
"p" #'proof-prf)
(:prefix ("p" . "proof")
"i" #'proof-interrupt-process
"p" #'proof-process-buffer
"q" #'proof-shell-exit
"r" #'proof-retract-buffer)
(:prefix ("a" . "about/print/check")
"a" #'coq-Print
"A" #'coq-Print-with-all
"b" #'coq-About
"B" #'coq-About-with-all
"c" #'coq-Check
"C" #'coq-Check-show-all
"f" #'proof-find-theorems
(:prefix ("i" . "implicits")
"b" #'coq-About-with-implicits
"c" #'coq-Check-show-implicits
"i" #'coq-Print-with-implicits))
(:prefix ("g" . "goto")
"e" #'proof-goto-command-end
"l" #'proof-goto-end-of-locked
"s" #'proof-goto-command-start)
(:prefix ("i" . "insert")
"c" #'coq-insert-command
"e" #'coq-end-Section
"i" #'coq-insert-intros
"r" #'coq-insert-requires
"s" #'coq-insert-section-or-module
"t" #'coq-insert-tactic
"T" #'coq-insert-tactical))
(after! company-coq
(set-popup-rule! "^\\*\\(?:response\\|goals\\)\\*" :ignore t)
@ -15,4 +54,15 @@
:references #'company-coq-grep-symbol
:documentation #'company-coq-doc)
(unless (featurep! :completion company)
(setq company-coq-disabled-features '(company company-defaults))))
(setq company-coq-disabled-features '(company company-defaults)))
(map! :map coq-mode-map
:localleader
(:prefix ("i" . "insert")
"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
"h" #'company-coq-doc)))