Skip to content

Commit

Permalink
feat(coq): add basic config for Coq
Browse files Browse the repository at this point in the history
Fixes #1007
  • Loading branch information
Fuco1 committed Jun 29, 2024
1 parent 470451b commit 236748c
Show file tree
Hide file tree
Showing 2 changed files with 61 additions and 0 deletions.
1 change: 1 addition & 0 deletions smartparens-config.el
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,7 @@ ID, ACTION, CONTEXT."
(eval-after-load 'cc-mode '(require 'smartparens-c))
(--each '(clojure-mode clojure-ts-mode)
(eval-after-load it '(require 'smartparens-clojure)))
(eval-after-load 'coq-mode '(require 'smartparens-coq))
(eval-after-load 'crystal-mode '(require 'smartparens-crystal))
(eval-after-load 'elixir-mode '(require 'smartparens-elixir))
(eval-after-load 'elixir-ts-mode '(require 'smartparens-elixir))
Expand Down
60 changes: 60 additions & 0 deletions smartparens-coq.el
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
;;; smartparens-coq.el --- Additional configuration for Coq proof assistant -*- lexical-binding: t; -*-

;; Copyright (C) 2024 Matus Goljer

;; Author: Matus Goljer <[email protected]>
;; Maintainer: Matus Goljer <[email protected]>
;; Created: 29 June 2024
;; Keywords: smartparens, coq
;; URL: https://github.com/Fuco1/smartparens

;; This file is not part of GNU Emacs.

;;; License:

;; This file is part of Smartparens.

;; Smartparens is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.

;; Smartparens is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with Smartparens. If not, see <http://www.gnu.org/licenses/>.

;;; Commentary:

;; This file provides some additional configuration for Coq proof
;; assistant. To use it, simply add:
;;
;; (require 'smartparens-coq)
;;
;; into your configuration. You can use this in conjunction with the
;; default config or your own configuration.
;;
;; If you have good ideas about what should be added please file an
;; issue on the github tracker.
;;
;; For more info, see github readme at
;; https://github.com/Fuco1/smartparens

;;; Code:

(require 'smartparens)

(sp-with-modes '(coq-mode)
;; Disable ' because it is used in pattern-matching
(sp-local-pair "'" nil :actions nil)
;; Disable ` because it is used in polymorphic variants
(sp-local-pair "`" nil :actions nil)
(sp-local-pair "(*" "*)"
:post-handlers '(("| " "SPC")
(" | " "*"))))

(provide 'smartparens-coq)
;;; smartparens-coq.el ends here

0 comments on commit 236748c

Please sign in to comment.