New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add configuration for Coq #1007
base: master
Are you sure you want to change the base?
Conversation
Is |
(sp-with-modes '(coq-mode) | ||
;; Disable ` because it is used in implicit generalization | ||
(sp-local-pair "`" nil :actions nil) | ||
(sp-local-pair "(*" "*)" :actions nil) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would be nice to also add:
;; Disable ' because it is used in pattern-matching
(sp-local-pair "'" nil :actions nil)
(sp-local-pair "(*" "*)" :actions nil) | ||
(sp-local-pair "(*" "*" | ||
:actions '(insert) | ||
:post-handlers '(("| " "SPC") ("|\n[i]*)[d-2]" "RET"))) ) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What does this do?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a tiny DSL which can specify certain actions to be performed after the pair was inserted and another command was triggered. See https://github.com/Fuco1/smartparens/wiki/Permissions#insertion-specification
This is somewhat magical to me but it's copied from Doom Emacs' configuration for OCaml (tuareg-mode) and F# and it seems to work nicely: https://github.com/hlissner/doom-emacs/blob/1ab9f8b99d35a451a06c8278457ddfa58c566186/modules/config/default/config.el#L182.
I also tried
(sp-local-pair "(*" "*)")
but with that if you type(*
you get(**))
. It's quite possible that smartparens has this bug currently for OCaml and F#.