Milestone 3.1: Delete Obsolete Code

Makefile

@@ -8,3 +8,6 @@ lean4-mode.info lean4-mode.texi: README.org
 		"--eval=(require 'ox-texinfo)" \
 		'--eval=(find-file "$<")' \
 		'--eval=(org-texinfo-export-to-info)'
+
+clean:
+	rm lean4-mode.info lean4-mode.texi

README.org

@@ -154,7 +154,7 @@ in VS-Code) in a separate window.
 |------------------------+--------------------------------------------------------+-----------------------------------|
 | =C-c C-k=              | Echo the keystroke needed to input the symbol at point | ~quail-show-key~                  |
 | =C-c C-d=              | Recompile and reload imports                           | ~lean4-refresh-file-dependencies~ |
-| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode                       | ~lean4-std-exe~                   |
+| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode                       | ~lean4-execute~                   |
 | =C-c C-p C-l=          | Builds package with lake                               | ~lean4-lake-build~                |
 | =C-c C-i=              | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~        |
 
@@ -200,3 +200,74 @@ reasons.  In principle, it is fine to have both Lean3-Mode and
 Lean4-Mode installed at the same time.  But note that Lean3-Mode uses
 the prefix =lean-= for its symbols.  E.g. you should not use
 =lean-=-prefixed commands in a buffer with Lean4-Mode as major mode.
+
+* Changelog
+
+** Upcoming Version
+
+Documentation:
+- The changelog is now part of the readme (and thus of the Info
+  manual).
+
+User interface:
+- The tool-bar menu of Lean4-Mode does not list the
+  ~flycheck-list-errors~ anymore. Please use the “Show all errors”
+  entry in Flycheck's menu instead. (Fixes [[https://github.com/leanprover-community/lean4-mode/issues/91][#91]].)
+
+Features:
+- The variable ~lean4-delete-trailing-whitespace~ has been removed
+  together with related code. Instead of reinventing the wheel,
+  Lean4-Mode demands users to use Emacs' built-in facilities for this
+  kind of use case. For example, you might want to define a function
+  that buffer-locally adds ~delete-trailing-whitespace~ to
+  ~before-save-hook~, and add that hereby defined function to
+  ~lean4-mode-hook~.
+- The variable ~lean4-autodetect-lean3~ has been removed along with
+  the command ~lean4-select-mode~ and related code. If you still use
+  legacy version 3 of Lean for some files or projects, you could
+  directory- or file-locally associate the =.lean= file extension with
+  Lean3-Mode in ~auto-mode-alist~.
+- The command ~lean4-show-version~ has been removed. Lean4-Mode now
+  assumes Lean version 4. In order to determine the minor version, you
+  may type =M-! lean --version RET= or similar.
+- The functions ~lean4-input-export-translations~ and
+  ~lean4-input-export-translations-to-stdout~ have been removed. We
+  expect that noone has been using it. If you do use it, let us know,
+  so we can reconsider our decision in case of a substantial amount of
+  users. Otherwise, please just define these functions in your Emacs
+  initialization file yourself.
+- The command ~lean4-std-exe~ has been removed. It was just the same
+  as ~lean4-execute~ which continues to exist.
+
+** Version 1.1.2 from 2024-12-10
+
+- Fix occasional errors like "The connected server(s) does not support
+  method =$/lean/plainGoal=" by not wrapping invocations of
+  ~lsp-protocol~ macro into ~eval-when-compile~ but rather into
+  ~eval-and-compile~.  Thus, the methods should now work, no matter
+  whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by
+  loading compiled =.elc= or =.eln= files.  ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]])
+
+** Version 1.1.1 from 2024-12-02
+
+- Assign all customizable user-options to the Lean4-Mode specific
+  =lean4= group.  To customize Lean4-Mode, you now need to type =M-x
+  customize-group RET lean4 RET=.
+
+** Version 1.1.0 from 2024-12-01
+
+- To =lean4= customization group, add link to local info manual and
+  use Lean4-Mode Github URL as website.
+- Introduce new dependency on Elpa package =compat=.
+- Remove dependency on Elpa package Flycheck.  It is still supported
+  but not required.
+
+** Version 1.0.1 from 2024-11-21
+
+- Specify Yury G. Kudryashov as maintainer.
+- Rework README.  (Now in Org format).
+- Provide README as Texi and Info manual too.
+
+** Version 1.0 from 2024-11-16
+
+- Specify "Version" in Emacs-Lisp library header.

lean4-input.el

@@ -307,37 +307,6 @@ Suitable for use in the :set field of `defcustom'."
 (cl-eval-when (load eval)
   (lean4-input-setup))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Export Translations
-
-(defun lean4-input-export-translations ()
-  "Export the current translations in a javascript format.
-Print (input, output) pairs in Javascript format to the buffer
-*lean4-translations*.  The output can be copy-pasted to
-leanprover.github.io/tutorial/js/input-method.js"
-  (interactive)
-  (with-current-buffer
-      (get-buffer-create "*lean4-translations*")
-    (let ((exclude-list '("\\newline")))
-      (insert "var corrections = {")
-      (--each
-          (--filter (not (member (car it) exclude-list))
-                    (lean4-input-get-translations "Lean"))
-        (let* ((input (substring (car it) 1))
-               (outputs (cdr it)))
-          (insert (format "%s:\"" (prin1-to-string input)))
-          (cond ((vectorp outputs)
-                 (insert (elt outputs 0)))
-                (t (insert-char outputs)))
-          (insert (format "\",\n"))))
-      (insert "};"))))
-
-(defun lean4-input-export-translations-to-stdout ()
-  "Print current translations to stdout."
-  (lean4-input-export-translations)
-  (with-current-buffer "*lean4-translations*"
-    (princ (buffer-string))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Administrative details
 

lean4-mode.el

@@ -63,7 +63,6 @@
 (defvar markdown-code-lang-modes)
 (declare-function flycheck-list-errors "ext:flycheck")
 (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc")
-(declare-function lean-mode "ext:lean-mode")
 (declare-function quail-show-key "quail")
 
 (defun lean4-compile-string (lake-name exe-name args file-name)
@@ -102,11 +101,6 @@ FILE-NAME."
     (setq compile-command cc)
     (setq default-directory dd)))
 
-(defun lean4-std-exe ()
-  "Execute Lean in the current buffer."
-  (interactive)
-  (lean4-execute))
-
 (defun lean4-refresh-file-dependencies ()
   "Refresh the file dependencies.
 
@@ -132,9 +126,9 @@ file, recompiling, and reloading all imports."
         (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)
+  "Setup Lean4 keybindings."
+  (local-set-key lean4-keybinding-std-exe1                  #'lean4-execute)
+  (local-set-key lean4-keybinding-std-exe2                  #'lean4-execute)
   (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)
@@ -147,9 +141,6 @@ file, recompiling, and reloading all imports."
   ;; (local-set-key (kbd "<mouse-3>")                         #'lean4-right-click-show-menu)
   )
 
-(define-abbrev-table 'lean4-abbrev-table
-  '())
-
 (defvar lean4-mode-map (make-sparse-keymap)
   "Keymap used in Lean mode.")
 
@@ -158,19 +149,11 @@ file, recompiling, and reloading all imports."
   `("Lean 4"
     ["Execute lean"         lean4-execute           t]
     ["Toggle info display"  lean4-toggle-info       t]
-    ;; TODO: Bug#91: We offers a Flycheck-based menu-item when
-    ;; Flycheck is in use.  Users who use built-in Flymake should also
-    ;; be offered a working menu-item.  Alternatively, the menu-item
-    ;; could also be dropped for both cases.
-    ["List of errors"       flycheck-list-errors    flycheck-mode]
     ["Restart lean process" lsp-workspace-restart   t]
     ["Customize lean4-mode" (customize-group 'lean) t]))
 
 (defconst lean4-hooks-alist
-  '(
-    ;; Handle events that may start automatic syntax checks
-    (before-save-hook . lean4-whitespace-cleanup)
-    ;; info view
+  '(;; info view
     ;; update errors immediately, but delay querying goal
     (flycheck-after-syntax-check-hook . lean4-info-buffer-redisplay-debounced)
     (post-command-hook . lean4-info-buffer-redisplay-debounced)
@@ -216,7 +199,6 @@ of the parent project."
 
 \\{lean4-mode-map}"
   :syntax-table lean4-syntax-table
-  :abbrev-table lean4-abbrev-table
   :group 'lean4
   (set (make-local-variable 'comment-start) "--")
   (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*")
@@ -234,41 +216,19 @@ of the parent project."
   (lean4-set-keys)
   (if (fboundp 'electric-indent-local-mode)
       (electric-indent-local-mode -1))
-  ;; (abbrev-mode 1)
   (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist)
     (add-hook hook fn nil 'local))
   (lean4-mode-setup))
 
-(defun lean4--version ()
-  "Return Lean version as a list `(MAJOR MINOR PATCH)'."
-  (with-temp-buffer
-    (call-process (lean4-get-executable "lean") nil (list t nil) nil "-v")
-    (goto-char (point-min))
-    (re-search-forward (rx bol "Lean (version " (group (+ digit) (+ "." (+ digit)))))
-    (version-to-list (match-string 1))))
-
-(defun lean4-show-version ()
-  "Print Lean 4 version."
-  (interactive)
-  (message "Lean %s" (mapconcat #'number-to-string (lean4--version) ".")))
-
-;;;###autoload
-(defun lean4-select-mode ()
-  "Automatically select mode (Lean 3 vs Lean 4)."
-  (if (and lean4-autodetect-lean3
-           (eq 3 (car (lean4--version))))
-      (lean-mode)
-    (lean4-mode)))
-
 ;; Automatically use lean4-mode for .lean files.
 ;;;###autoload
 (add-to-list 'auto-mode-alist
-             '("\\.lean\\'" . lean4-select-mode))
+             '("\\.lean\\'" . lean4-mode))
 
 ;;;###autoload
 (with-eval-after-load 'markdown-mode
   (add-to-list 'markdown-code-lang-modes
-               '("lean" . lean4-select-mode)))
+               '("lean" . lean4-mode)))
 
 ;; Use utf-8 encoding
 ;;;### autoload