Some proof fixes and ACME tweaks

2 files changed, 69 insertions, 38 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))
diff --git a/emacs/themes/acme-theme.el b/emacs/themes/acme-theme.el
index ad5baab..c375ab8 100644
--- a/emacs/themes/acme-theme.el
+++ b/emacs/themes/acme-theme.el
@@ -22,12 +22,10 @@
 (deftheme acme
   "A theme inspired by the classic colours of the ACME editor.")
 
-(let ((bg-yellow "#FFFFCA")
-      (bg-blue "#DAEFEF")
-      
+(let ((bg-yellow "#FFFFEA")
+      (bg-blue "#EAFFFF")
       (lazy "#D1D1C0")
       (mud "#99994C")
-      
       (yellow "#EAEA9E")
       (blue "#268BD2")
       (red "#AA0000")
@@ -36,7 +34,6 @@
       (link "#D05000"))
   (custom-theme-set-faces
    'acme
-   
    `(default ((t (:background ,bg-yellow :foreground "black"))))
    '(cursor ((t (:background "black"))))
    '(escape-glyph ((t (:foreground "black"))))
@@ -45,14 +42,12 @@
    `(region ((t (:background ,yellow :foreground "black"))))
    `(secondary-selection ((t (:background ,red))))
    '(trailing-whitespace ((t (:background "grey"))))
-   
+
+   '(font-lock-comment-face ((t (:foreground "black" :slant italic))))
    '(font-lock-builtin-face ((t (:foreground "black" :slant normal))))
    '(font-lock-comment-delimiter-face ((default (:inherit (font-lock-comment-face)))))
-   '(font-lock-comment-face ((t (:foreground "black" :slant italic
-                                             :font "Hack"))))
    '(font-lock-constant-face ((t (:foreground "black"))))
-   '(font-lock-doc-face ((t (:foreground "black" :slant italic
-                                         :font "Hack"))))
+   '(font-lock-doc-face ((t (:foreground "black" :slant italic))))
    '(font-lock-function-name-face ((t (:foreground "black" :weight bold))))
    '(font-lock-keyword-face ((t (:foreground "black" :weight bold))))
    '(font-lock-negation-char-face ((t (:foreground "black"))))
@@ -61,20 +56,29 @@
    '(font-lock-type-face ((t (:foreground "black" :underline t))))
    '(font-lock-variable-name-face ((t (:foreground "black"))))
    '(font-lock-warning-face ((t (:foreground "black"))))
-   
+
    '(button ((t (:inherit (link)))))
-   `(link ((t (:underline (:color foreground-color :style line)
-                          :foreground ,link))))
+   `(link ((t (:underline (:color foreground-color :style line) :foreground ,link))))
    '(link-visited ((default (:inherit (link)))
                    (((class color) (background light)) (:foreground "magenta4"))
                    (((class color) (background dark)) (:foreground "violet"))))
-   
+
    `(fringe ((t (:background ,bg-yellow :foreground "black"))))
-   '(header-line ((default (:inherit (mode-line))) (((type tty)) (:underline (:color foreground-color :style line) :inverse-video nil)) (((class color grayscale) (background light)) (:box nil :foreground "grey20" :background "grey90")) (((class color grayscale) (background dark)) (:box nil :foreground "grey90" :background "grey20")) (((class mono) (background light)) (:underline (:color foreground-color :style line) :box nil :inverse-video nil :foreground "black" :background "white")) (((class mono) (background dark)) (:underline (:color foreground-color :style line) :box nil :inverse-video nil :foreground "white" :background "black"))))
-   '(tooltip ((((class color))
-               (:inherit (variable-pitch) :foreground "black" :background "lightyellow"))
+
+   '(header-line ((default (:inherit (mode-line)))
+                  (((type tty)) (:underline (:color foreground-color :style line) :inverse-video nil))
+                  (((class color grayscale) (background light)) (:box nil :foreground "grey20" :background "grey90"))
+                  (((class color grayscale) (background dark)) (:box nil :foreground "grey90" :background "grey20"))
+                  (((class mono) (background light)) (:underline (:color foreground-color :style line)
+                                                                 :box nil :inverse-video nil
+                                                                 :foreground "black" :background "white"))
+                  (((class mono) (background dark)) (:underline (:color foreground-color :style line)
+                                                                :box nil :inverse-video nil
+                                                                :foreground "white" :background "black"))))
+
+   '(tooltip ((((class color)) (:inherit (variable-pitch) :foreground "black" :background "lightyellow"))
               (t (:inherit (variable-pitch)))))
-   
+
    `(mode-line ((t (:background ,bg-blue :foreground "black" :box 2))))
    '(mode-line-buffer-id ((t (:foreground "black" :weight bold))))
    '(mode-line-emphasis ((t (:foreground "black"))))
@@ -88,30 +92,28 @@
    '(next-error ((t (:inherit (region)))))
    '(query-replace ((t (:inherit (isearch)))))
    '(table-cell  ((t (:inherit (default)))))
-   
+
    `(show-paren-match ((t (:weight bold :background ,purple))))
    `(show-paren-mismatch ((t (:background ,red))))
    `(sp-show-pair-match-face ((t (:weight bold :background ,purple))))
    `(sp-show-pair-mismatch-face ((t (:background ,red))))
 
    '(ivy-modified-buffer ((t (:underline t :inherit (default)))))
-   
+
    `(company-echo-common ((t (:foreground "black" :background ,bg-blue :weight bold))))
    `(company-scrollbar-bg ((t (:background "grey"))))
    `(company-scrollbar-fg ((t (:background ,green))))
    `(company-tooltip ((t (:foreground "black" :background ,bg-blue))))
    `(company-tooltip-search ((t (:foreground "black" :background ,yellow))))
-   `(company-tooltip-annotation ((t (:foreground "black" :background "grey" :slant italic))))
+   `(company-tooltip-annotation ((t (:foreground ,link :slant italic))))
    `(company-tooltip-common ((t (:foreground "black" :weight bold))))
-   `(company-tooltip-common-selection ((t (:foreground "black" :background ,yellow :weight bold))))
+   `(company-tooltip-common-selection ((t (:foreground "black" :background
+                                                       ,yellow :weight bold))))
    `(company-tooltip-selection ((t (:background ,yellow :foreground "black"))))
 
    '(font-latex-bold-face ((t (:weight bold))))
    '(font-latex-italic-face ((t (:slant italic))))
-   `(font-latex-math-face ((t (:foreground "black"
-                                           :box (:line-width 2 :color ,lazy
-                                                             :style pressed-button)
-                                           :foreground "black"))))
+   '(font-latex-math-face ((t (:foreground "black" :box (:line-width 1 :color "grey" :style sunken)))))
    '(font-latex-string-face ((t (:foreground "black"))))
    '(font-latex-verbatim-face ((t (:foreground "black"))))
    '(font-latex-sedate-face ((t (:foreground "black"))))
@@ -127,12 +129,9 @@
    `(avy-lead-face-1 ((t (:background ,red))))
    `(avy-lead-face-2 ((t (:background ,purple))))
 
-   '(company-coq-comment-h1-face ((t (:height 1.8 :slant italic
-                                              :inherit (default)))))
-   '(company-coq-comment-h2-face ((t (:height 1.4 :slant italic
-                                              :inherit (default)))))
-   '(company-coq-comment-h3-face ((t (:height 1.2 :slant italic
-                                              :inherit (default)))))
+   '(company-coq-comment-h1-face ((t (:height 1.8 :slant italic :inherit (default)))))
+   '(company-coq-comment-h2-face ((t (:height 1.4 :slant italic :inherit (default)))))
+   '(company-coq-comment-h3-face ((t (:height 1.2 :slant italic :inherit (default)))))
    '(company-coq-coqdoc-h1-face ((t (:weight bold :inverse-video t))))
    '(company-coq-coqdoc-h2-face ((t (:weight bold :underline t))))
    '(company-coq-coqdoc-h3-face ((t (:underline t))))
@@ -140,7 +139,7 @@
 
    '(company-coq-features/code-folding-bullet-face
      ((t (:foreground "black" :weight bold))))
-   
+
    `(coq-solve-tactics-face ((t (:foreground "black" :underline t))))
    `(proof-tactics-name-face ((t (:foreground "black" :weight bold))))
    ))