|
| 1 | +;;; smartparens-coq.el --- Additional configuration for Coq proof assistant -*- lexical-binding: t; -*- |
| 2 | + |
| 3 | +;; Copyright (C) 2024 Matus Goljer |
| 4 | + |
| 5 | +;; Author: Matus Goljer <[email protected]> |
| 6 | +;; Maintainer: Matus Goljer <[email protected]> |
| 7 | +;; Created: 29 June 2024 |
| 8 | +;; Keywords: smartparens, coq |
| 9 | +;; URL: https://github.com/Fuco1/smartparens |
| 10 | + |
| 11 | +;; This file is not part of GNU Emacs. |
| 12 | + |
| 13 | +;;; License: |
| 14 | + |
| 15 | +;; This file is part of Smartparens. |
| 16 | + |
| 17 | +;; Smartparens is free software; you can redistribute it and/or modify |
| 18 | +;; it under the terms of the GNU General Public License as published by |
| 19 | +;; the Free Software Foundation, either version 3 of the License, or |
| 20 | +;; (at your option) any later version. |
| 21 | + |
| 22 | +;; Smartparens is distributed in the hope that it will be useful, |
| 23 | +;; but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 24 | +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 25 | +;; GNU General Public License for more details. |
| 26 | + |
| 27 | +;; You should have received a copy of the GNU General Public License |
| 28 | +;; along with Smartparens. If not, see <http://www.gnu.org/licenses/>. |
| 29 | + |
| 30 | +;;; Commentary: |
| 31 | + |
| 32 | +;; This file provides some additional configuration for Coq proof |
| 33 | +;; assistant. To use it, simply add: |
| 34 | +;; |
| 35 | +;; (require 'smartparens-coq) |
| 36 | +;; |
| 37 | +;; into your configuration. You can use this in conjunction with the |
| 38 | +;; default config or your own configuration. |
| 39 | +;; |
| 40 | +;; If you have good ideas about what should be added please file an |
| 41 | +;; issue on the github tracker. |
| 42 | +;; |
| 43 | +;; For more info, see github readme at |
| 44 | +;; https://github.com/Fuco1/smartparens |
| 45 | + |
| 46 | +;;; Code: |
| 47 | + |
| 48 | +(require 'smartparens) |
| 49 | + |
| 50 | +(sp-with-modes '(coq-mode) |
| 51 | + ;; Disable ' because it is used in pattern-matching |
| 52 | + (sp-local-pair "'" nil :actions nil) |
| 53 | + ;; Disable ` because it is used in polymorphic variants |
| 54 | + (sp-local-pair "`" nil :actions nil) |
| 55 | + (sp-local-pair "(*" "*)" |
| 56 | + :post-handlers '(("| " "SPC") |
| 57 | + (" | " "*")))) |
| 58 | + |
| 59 | +(provide 'smartparens-coq) |
| 60 | +;;; smartparens-coq.el ends here |
0 commit comments