Dissolve lean4-settings

Fixes issue #88 "Remove lean4-keybinding-* user options and dissolve
other parts of
lean4-settings.el"
(<#88>).

lean4-fringe.el

@@ -22,7 +22,6 @@
 
 ;;; Code:
 
-(require 'lean4-settings)
 (require 'lsp-mode)
 (require 'lsp-protocol)
 
@@ -70,6 +69,11 @@
 
 (defvar-local lean4-fringe-data nil)
 
+(defcustom lean4-show-file-progress t
+  "Highlight file progress in the current buffer."
+  :group 'lean4
+  :type 'boolean)
+
 (defun lean4-fringe-update-progress-overlays ()
   "Update processing bars in the current buffer."
   (dolist (ov (flatten-tree (overlay-lists)))

lean4-info.el

@@ -24,7 +24,6 @@
 
 (require 'dash)
 (require 'lean4-syntax)
-(require 'lean4-settings)
 (require 'lsp-mode)
 (require 'lsp-protocol)
 (require 'magit-section)
@@ -100,6 +99,13 @@ The buffer is supposed to be the *Lean Goal* buffer."
       (forward-line (1- line))
       (forward-char column))))
 
+(defcustom lean4-highlight-inaccessible-names t
+  "Use font to highlight inaccessible names.
+Set this variable to t to highlight inaccessible names in the info display
+using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
+  :group 'lean4
+  :type 'boolean)
+
 (defun lean4-info--insert-highlight-inaccessible-names (&rest text)
   (let ((begin (point)))
     (apply #'insert text)

lean4-lake.el

@@ -22,7 +22,12 @@
 ;;; Code:
 
 (require 'lean4-util)
-(require 'lean4-settings)
+
+(defcustom lean4-lake-name
+  (if (eq system-type 'windows-nt) "lake.exe" "lake")
+  "Name of lake executable."
+  :group 'lake
+  :type 'string)
 
 (defun lean4-lake-find-dir-in (dir)
   "Find a parent directory of DIR with file \"lakefile.lean\"."

lean4-mode.el

@@ -49,7 +49,6 @@
 (require 'lean4-fringe)
 (require 'lean4-info)
 (require 'lean4-lake)
-(require 'lean4-settings)
 (require 'lean4-syntax)
 (require 'lean4-util)
 
@@ -69,6 +68,16 @@
 (declare-function lean-mode "ext:lean-mode")
 (declare-function quail-show-key "quail")
 
+(defgroup lean4 nil
+  "Major mode for Lean4 programming language and theorem prover."
+  :group 'languages
+  :link '(info-link :tag "Info Manual" "(lean4-mode)")
+  :link '(url-link
+          :tag "Website"
+          "https://github.com/leanprover-community/lean4-mode")
+  :link '(emacs-library-link :tag "Library Source" "lean4-mode.el")
+  :prefix "lean4-")
+
 (defun lean4-compile-string (lake-name exe-name args file-name)
   "Command to run EXE-NAME with extra ARGS and FILE-NAME.
 If LAKE-NAME is nonempty, then prepend \"LAKE-NAME env\" to the command
@@ -271,6 +280,14 @@ added here because it will be called by `lsp' if the variable
   (interactive)
   (message "Lean %s" (mapconcat #'number-to-string (lean4--version) ".")))
 
+(defcustom lean4-autodetect-lean3 nil
+  "Autodetect Lean version.
+Use elan to check if current project uses Lean 3 or Lean 4 and initialize the
+right mode when visiting a file.  If elan has a default Lean version, Lean files
+outside a project will default to that mode."
+  :group 'lean4
+  :type 'boolean)
+
 ;;;###autoload
 (defun lean4-select-mode ()
   "Automatically select mode (Lean 3 vs Lean 4)."

lean4-util.el

@@ -23,7 +23,17 @@
 ;;; Code:
 
 (require 'compat)
-(require 'lean4-settings)
+
+(defcustom lean4-executable-name
+  (if (eq system-type 'windows-nt) "lean.exe" "lean")
+  "Name of lean executable."
+  :group 'lean4
+  :type 'string)
+
+(defcustom lean4-rootdir nil
+  "Full pathname of lean root directory.  It should be defined by user."
+  :group 'lean4
+  :type 'string)
 
 (defun lean4-setup-rootdir ()
   "Search for lean executable in variable `exec-path'.
@@ -55,6 +65,14 @@ First try to find an executable named `lean4-executable-name' in
   "Return fullpath of lean executable EXE-NAME."
   (file-name-concat (lean4-get-rootdir) "bin" exe-name))
 
+(defcustom lean4-delete-trailing-whitespace nil
+  "Automatically delete trailing shitespace.
+Set this variable to true to automatically delete trailing
+whitespace when a buffer is loaded from a file or when it is
+written."
+  :group 'lean4
+  :type 'boolean)
+
 (defun lean4-whitespace-cleanup ()
   "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t."
   (when lean4-delete-trailing-whitespace