Some proof fixes and ACME tweaks

1 files changed, 37 insertions, 5 deletions

diff --git a/emacs/inits/25-theorems.el b/emacs/inits/25-theorems.el
index 614a4b2..b72dabc 100644
--- a/emacs/inits/25-theorems.el
+++ b/emacs/inits/25-theorems.el
@@ -1,4 +1,4 @@
-;; Time-stamp: <2019-09-18 11:36:11 (tslil@basingstoke)>
+;; Time-stamp: <2020-01-06 20:36:12 (tslil@bison)>
 
 ;; -----------------------------------------------------------------------------
 ;; Coq
@@ -45,7 +45,26 @@
                      :binary "hoqtop"
                      :args nil)))
 
-(defvar use-coq-env "UniMath")
+(defvar use-coq-env "HoTT")
+
+(defun mike-implicify (ntimes)
+  (interactive "p")
+  (save-excursion
+    (dotimes (i ntimes)
+      (re-search-backward "(\\|{")
+      (if (looking-at "(")
+          (progn (delete-char 1)
+                 (insert "{")
+                 (backward-char 1)
+                 (forward-sexp 1)
+                 (delete-char -1)
+                 (insert "}"))
+        (progn (delete-char 1)
+               (insert "(")
+               (backward-char 1)
+               (forward-sexp 1)
+               (delete-char -1)
+               (insert ")"))))))
 
 (use-package proof-general
   :ensure t
@@ -58,10 +77,23 @@
   ;; numbers and the like
   (defadvice proof-layout-windows (after resize-window-properly activate)
     (let ((ww (window-width)))
-      (when (< ww (+ 5 fill-column))
-        (enlarge-window-horizontally (- (+ 5 fill-column) ww)))))
+      (when (< ww (+ 7 fill-column))
+        (enlarge-window-horizontally (- (+ 7 fill-column) ww)))))
   (defun coq-local-environment ()
-    (bind-key "C-s" #'isearch-forward proof-mode-map)
+    (require 'corral)
+    (bind-keys ("M-i" . mike-implicify)
+               ("M-a" . forward-sexp)
+               ("M-e" . backward-sexp)
+               ("M-/" . lh-matching-delim)
+               ("M-(" . corral-parentheses-forward)
+               ("M-)" . corral-parentheses-backward)
+               ("M-{" . corral-braces-forward)
+               ("M-}" . corral-braces-backward)
+               ("M-[" . corral-brackets-forward)
+               ("M-]" . corral-brackets-backward)
+               ("C-(" . lh-slurp-forward)
+               ("C-)" . lh-slurp-backward)
+               ("C-s" . isearch-forward-proof-mode-map))
     (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))