diff options
| author | tslil clingman <> | 2020-01-12 11:46:40 -0500 |
|---|---|---|
| committer | tslil clingman <> | 2020-01-12 11:46:40 -0500 |
| commit | 800b2b1a51c77a328042f47d24e2517266029544 (patch) | |
| tree | 03e0724f7425af1e892a1ac6551fd762feb1a7db /emacs/inits/25-theorems.el | |
| parent | a86d9385f37b8705fe9e9cf98361a129e2bfe0b3 (diff) | |
Changes from using bison
Diffstat (limited to 'emacs/inits/25-theorems.el')
| -rw-r--r-- | emacs/inits/25-theorems.el | 14 |
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) |
