From d08f27127d304671919c409658eeb5fdf8be3e43 Mon Sep 17 00:00:00 2001
From: Mekeor Melire <mekeor@posteo.de>
Date: Fri, 6 Dec 2024 11:14:25 +0100
Subject: [PATCH] Remove lean4-keybindings-* variables and related code

Part of issue #88 "Remove lean4-keybinding-* user options and dissolve
other parts of
lean4-settings.el" (https://github.com/leanprover-community/lean4-mode/issues/88).
---
 lean4-mode.el     | 28 +++++++++-------------------
 lean4-settings.el | 33 ---------------------------------
 2 files changed, 9 insertions(+), 52 deletions(-)

diff --git a/lean4-mode.el b/lean4-mode.el
index e300343..d9c1595 100644
--- a/lean4-mode.el
+++ b/lean4-mode.el
@@ -132,24 +132,15 @@ file, recompiling, and reloading all imports."
          (lean4-eri-indent))
         (t (indent-for-tab-command))))
 
-(defun lean4-set-keys ()
-  "Setup Lean 4 keybindings."
-  (local-set-key lean4-keybinding-std-exe1                  #'lean4-std-exe)
-  (local-set-key lean4-keybinding-std-exe2                  #'lean4-std-exe)
-  (local-set-key lean4-keybinding-show-key                  #'quail-show-key)
-  (local-set-key lean4-keybinding-tab-indent                #'lean4-tab-indent)
-  ;; (local-set-key lean4-keybinding-hole                      #'lean4-hole)
-  (local-set-key lean4-keybinding-lean4-toggle-info         #'lean4-toggle-info)
-  ;; (local-set-key lean4-keybinding-lean4-message-boxes-toggle #'lean4-message-boxes-toggle)
-  (local-set-key lean4-keybinding-lake-build                #'lean4-lake-build)
-  (local-set-key lean4-keybinding-refresh-file-dependencies #'lean4-refresh-file-dependencies)
-  ;; This only works as a mouse binding due to the event, so it is not abstracted
-  ;; to avoid user confusion.
-  ;; (local-set-key (kbd "<mouse-3>")                         #'lean4-right-click-show-menu)
-  )
-
-(defvar lean4-mode-map (make-sparse-keymap)
-  "Keymap used in Lean mode.")
+(defvar-keymap lean4-mode-map
+  :doc "Keymap for `lean4-mode'."
+  "C-c C-x"     #'lean4-std-exe
+  "C-c C-l"     #'lean4-std-exe
+  "C-c C-k"     #'quail-show-key
+  "TAB"         #'lean4-tab-indent
+  "C-c C-i"     #'lean4-toggle-info
+  "C-c C-p C-l" #'lean4-lake-build
+  "C-c C-d"     #'lean4-refresh-file-dependencies)
 
 (easy-menu-define lean4-mode-menu lean4-mode-map
   "Menu for the Lean major mode."
@@ -228,7 +219,6 @@ of the parent project."
   (set-input-method "Lean")
   (set (make-local-variable 'lisp-indent-function)
        'common-lisp-indent-function)
-  (lean4-set-keys)
   (if (fboundp 'electric-indent-local-mode)
       (electric-indent-local-mode -1))
   (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist)
diff --git a/lean4-settings.el b/lean4-settings.el
index 910e533..ae33d8e 100644
--- a/lean4-settings.el
+++ b/lean4-settings.el
@@ -35,11 +35,6 @@
   :link '(emacs-library-link :tag "Library Source" "lean4-mode.el")
   :prefix "lean4-")
 
-(defgroup lean4-keybinding nil
-  "Keybindings for lean4-mode."
-  :prefix "lean4-"
-  :group 'lean4)
-
 (defconst lean4-default-executable-name
   (cl-case system-type
     (windows-nt "lean.exe")
@@ -119,33 +114,5 @@ outside a project will default to that mode."
   :group 'lean4
   :type 'boolean)
 
-(defcustom lean4-keybinding-std-exe1 (kbd "C-c C-x")
-  "Main Keybinding for `lean4-std-exe'."
-  :group 'lean4-keybinding :type 'key-sequence)
-(defcustom lean4-keybinding-std-exe2 (kbd "C-c C-l")
-  "Alternative Keybinding for `lean4-std-exe'."
-  :group 'lean4-keybinding  :type 'key-sequence)
-(defcustom lean4-keybinding-show-key (kbd "C-c C-k")
-  "Lean Keybinding for `quail-show-key'."
-  :group 'lean4-keybinding  :type 'key-sequence)
-(defcustom lean4-keybinding-server-restart (kbd "C-c C-r")
-  "Lean Keybinding for server-restart."
-  :group 'lean4-keybinding  :type 'key-sequence)
-(defcustom lean4-keybinding-tab-indent (kbd "TAB")
-  "Lean Keybinding for `lean4-tab-indent'."
-  :group 'lean4-keybinding  :type 'key-sequence)
-(defcustom lean4-keybinding-auto-complete (kbd "S-SPC")
-  "Lean Keybinding for auto completion."
-  :group 'lean4-keybinding  :type 'key-sequence)
-(defcustom lean4-keybinding-lean4-toggle-info (kbd "C-c C-i")
-  "Lean Keybinding for `lean4-toggle-info'."
-  :group 'lean4-keybinding  :type 'key-sequence)
-(defcustom lean4-keybinding-lake-build (kbd "C-c C-p C-l")
-  "Lean Keybinding for `lean4-lake-build'."
-  :group 'lean4-keybinding :type 'key-sequence)
-(defcustom lean4-keybinding-refresh-file-dependencies (kbd "C-c C-d")
-  "Lean Keybinding for `lean4-refresh-file-dependencies'."
-  :group 'lean4-keybinding :type 'key-sequence)
-
 (provide 'lean4-settings)
 ;;; lean4-settings.el ends here