From 2527306069d122478acf118a5ce0b19bbbd5bc05 Mon Sep 17 00:00:00 2001
From: Rudi Grinberg <rudi.grinberg@gmail.com>
Date: Sat, 7 Sep 2019 15:27:20 +0900
Subject: [PATCH] Use map! with after! to setup bindings

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
---
 modules/lang/lean/config.el | 53 +++++++++++++++++++------------------
 1 file changed, 27 insertions(+), 26 deletions(-)

diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el
index faf37150c..676bf3534 100644
--- a/modules/lang/lean/config.el
+++ b/modules/lang/lean/config.el
@@ -1,33 +1,34 @@
 ;;; lang/lean/config.el -*- lexical-binding: t; -*-
 
-(use-package! company-lean
-  :when (featurep :completion 'company)
-  :after lean-mode
-  :config (set-company-backend! 'lean-mode 'company-lean))
-
-(use-package! lean-mode
-  :config
+(after! lean-mode
   (set-lookup-handlers! 'lean-mode
     :definition #'lean-find-definition)
   (sp-with-modes 'lean-mode
     (sp-local-pair "/-" "-/")
-    (sp-local-pair "`'" nil :actions :rem)
+    (sp-local-pair "`" "`")
     (sp-local-pair "{" "}")
-    (sp-local-pair "«" "»"))
-  (map!
-   :map lean-mode-map
-   :localleader
-   "g" #'lean-toggle-show-goal
-   "n" #'lean-toggle-next-error
-   (:prefix "s"
-     "r" #'lean-server-restart
-     "s" #'lean-server-stop
-     "v" #'lean-server-switch-version)
-   (:prefix "p"
-     "t" #'lean-leanpkg-test
-     "b" #'lean-leanpkg-build
-     "c" #'lean-leanpkg-configure)
-   "f" #'lean-fill-placeholder
-   "h" #'lean-hole
-   "m" #'lean-message-boxes-toggle
-   "e" #'lean-execute))
+    (sp-local-pair "«" "»")
+    (sp-local-pair "⟨" "⟩")
+    (sp-local-pair "⟪" "⟫"))
+  (map! :map lean-mode-map
+        :localleader
+        "g" #'lean-toggle-show-goal
+        "n" #'lean-toggle-next-error
+        (:prefix ("s" . "server")
+          "r" #'lean-server-restart
+          "s" #'lean-server-stop
+          "v" #'lean-server-switch-version)
+        (:prefix ("p" . "leanpkg")
+          "t" #'lean-leanpkg-test
+          "b" #'lean-leanpkg-build
+          "c" #'lean-leanpkg-configure)
+        "f" #'lean-fill-placeholder
+        "h" #'lean-hole
+        "m" #'lean-message-boxes-toggle
+        "e" #'lean-execute))
+
+
+(use-package! company-lean
+  :when (featurep! :completion company)
+  :after lean-mode
+  :config (set-company-backend! 'lean-mode 'company-lean))