From 9e6162a74a18699b7d1e97478bdbf5cd570ded3a Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Mon, 9 Dec 2024 00:15:24 +0100 Subject: [PATCH] Dissolve lean4-settings Fixes issue #88 "Remove lean4-keybinding-* user options and dissolve other parts of lean4-settings.el" (). --- lean4-fringe.el | 6 ++- lean4-info.el | 8 +++- lean4-lake.el | 7 +++- lean4-mode.el | 19 ++++++++- lean4-settings.el | 101 ---------------------------------------------- lean4-util.el | 20 ++++++++- 6 files changed, 55 insertions(+), 106 deletions(-) delete mode 100644 lean4-settings.el diff --git a/lean4-fringe.el b/lean4-fringe.el index e5ab9e0..851f6a1 100644 --- a/lean4-fringe.el +++ b/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))) diff --git a/lean4-info.el b/lean4-info.el index 923cf56..37830a7 100644 --- a/lean4-info.el +++ b/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) diff --git a/lean4-lake.el b/lean4-lake.el index bfca627..1d0ced9 100644 --- a/lean4-lake.el +++ b/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\"." diff --git a/lean4-mode.el b/lean4-mode.el index 336cd0b..9d6c61a 100644 --- a/lean4-mode.el +++ b/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)." diff --git a/lean4-settings.el b/lean4-settings.el deleted file mode 100644 index e8f0f10..0000000 --- a/lean4-settings.el +++ /dev/null @@ -1,101 +0,0 @@ -;;; lean4-settings.el --- Lean4-Mode User-Options -*- lexical-binding: t; -*- - -;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library defines custom variables for `lean4-mode'. - -;;; Code: - -(require 'lsp-mode) - -(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-") - -(defcustom lean4-rootdir nil - "Full pathname of lean root directory. It should be defined by user." - :group 'lean4 - :type 'string) - -(defcustom lean4-executable-name - (if (eq system-type 'windows-nt) "lean.exe" "lean") - "Name of lean executable." - :group 'lean4 - :type 'string) - -(defcustom lean4-lake-name - (if (eq system-type 'windows-nt) "lake.exe" "lake") - "Name of lake executable." - :group 'lake - :type 'string) - -(defcustom lean4-memory-limit 1024 - "Memory limit for lean process in megabytes." - :group 'lean4 - :type 'number) - -(defcustom lean4-timeout-limit 100000 - "Deterministic timeout limit. - -It is approximately the maximum number of memory allocations in thousands." - :group 'lean4 - :type 'number) - -(defcustom lean4-extra-arguments nil - "Extra command-line arguments to the lean process." - :group 'lean4 - :type '(list string)) - -(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) - -(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) - -(defcustom lean4-show-file-progress t - "Highlight file progress in the current buffer." - :group 'lean4 - :type 'boolean) - - -(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) - -(provide 'lean4-settings) -;;; lean4-settings.el ends here diff --git a/lean4-util.el b/lean4-util.el index 273a530..79cfa7f 100644 --- a/lean4-util.el +++ b/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