summaryrefslogtreecommitdiff
path: root/emacs/inits/25-theorems.el
diff options
context:
space:
mode:
authortslil clingman <>2020-01-12 11:46:40 -0500
committertslil clingman <>2020-01-12 11:46:40 -0500
commit800b2b1a51c77a328042f47d24e2517266029544 (patch)
tree03e0724f7425af1e892a1ac6551fd762feb1a7db /emacs/inits/25-theorems.el
parenta86d9385f37b8705fe9e9cf98361a129e2bfe0b3 (diff)
Changes from using bison
Diffstat (limited to 'emacs/inits/25-theorems.el')
-rw-r--r--emacs/inits/25-theorems.el14
1 files changed, 9 insertions, 5 deletions
diff --git a/emacs/inits/25-theorems.el b/emacs/inits/25-theorems.el
index b72dabc..f5ab26b 100644
--- a/emacs/inits/25-theorems.el
+++ b/emacs/inits/25-theorems.el
@@ -1,4 +1,4 @@
-;; Time-stamp: <2020-01-06 20:36:12 (tslil@bison)>
+;; Time-stamp: <2020-01-08 18:37:56 (tslil@bison)>
;; -----------------------------------------------------------------------------
;; Coq
@@ -50,8 +50,8 @@
(defun mike-implicify (ntimes)
(interactive "p")
(save-excursion
+ (re-search-backward "(\\|{")
(dotimes (i ntimes)
- (re-search-backward "(\\|{")
(if (looking-at "(")
(progn (delete-char 1)
(insert "{")
@@ -64,7 +64,9 @@
(backward-char 1)
(forward-sexp 1)
(delete-char -1)
- (insert ")"))))))
+ (insert ")")))
+ (re-search-forward "(\\|{")
+ (backward-char 1))))
(use-package proof-general
:ensure t
@@ -81,7 +83,8 @@
(enlarge-window-horizontally (- (+ 7 fill-column) ww)))))
(defun coq-local-environment ()
(require 'corral)
- (bind-keys ("M-i" . mike-implicify)
+ (bind-keys :map coq-mode-map
+ ("M-i" . mike-implicify)
("M-a" . forward-sexp)
("M-e" . backward-sexp)
("M-/" . lh-matching-delim)
@@ -93,7 +96,7 @@
("M-]" . corral-brackets-backward)
("C-(" . lh-slurp-forward)
("C-)" . lh-slurp-backward)
- ("C-s" . isearch-forward-proof-mode-map))
+ ("C-s" . isearch-forward))
(let* ((data (alist-get use-coq-env coq-env nil nil #'string-equal))
(topdir (expand-file-name (plist-get data :topdir)))
(binary (plist-get data :binary))
@@ -102,6 +105,7 @@
(visit-tags-table (concat topdir "TAGS"))
;; Formatting
(setq fill-column 70)
+ (visual-line-mode 1)
(set-fringe-mode 0)
(make-local-variable 'before-save-hook)
(add-hook 'before-save-hook 'delete-trailing-whitespace)