Milestone 3: Breaking Refactor

.dir-locals.el

@@ -1,5 +1,5 @@
-;; -*- no-byte-compile: t; -*-
+;;; Directory Local Variables            -*- no-byte-compile: t -*-
+;;; For more information see (info "(emacs) Directory Variables")
 
-((nil
-  (bug-reference-url-format
-   . "https://github.com/leanprover-community/lean4-mode/issues/%s")))
+((nil . ((bug-reference-url-format . "https://github.com/leanprover-community/lean4-mode/issues/%s")))
+ (emacs-lisp-mode . ((indent-tabs-mode . nil))))

README.org

@@ -1,20 +1,16 @@
-#+title: Lean4-Mode - Emacs major mode for Lean language
+#+title: Emacs Lean4-Mode
 #+language: en
 #+export_file_name: lean4-mode.texi
 #+texinfo_dir_category: Emacs misc features
 #+texinfo_dir_title: Lean4-Mode: (lean4-mode).
 #+texinfo_dir_desc: Emacs major mode for Lean language
 
-This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by providing a major mode for editing
-code written in version 4 of the programming language and theorem
-prover [[https://lean-lang.org][Lean]].
+This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by a major mode for [[https://lean-lang.org][Lean]] version 4, a
+programming language and theorem prover.
 
-The Lean4-Mode source code is developed at [[https://github.com/leanprover-community/lean4-mode][Github]] and its issues
-tracked there too.  Further discussions and question-answering takes
-place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat.
-
-For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (also known
-as /Lean-Mode/).
+Lean4-Mode is developed on [[https://github.com/leanprover-community/lean4-mode][Github]].  Bugs and feature requests are also
+tracked there.  Further discussions take place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs]] channel
+on the Lean Zulip chat platform.
 
 * Installation
 
@@ -147,7 +143,7 @@ then type =#check id=, the word =#check= will be underlined, and
 hovering over it will show you the type of ~id~.
 
 To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=).  This
-will display the =*Lean Goals*= buffer (like the Lean Info-View pane
+will display the =*Lean4 Info*= buffer (like the Lean Info-View pane
 in VS-Code) in a separate window.
 
 | Key                    | Description                                            | Command                           |
@@ -194,9 +190,55 @@ option accordingly.
 
 * Common Pitfalls
 
-Lean4-Mode only supports version 4 of Lean.  For editing Lean version
-3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as Lean-Mode due to historical
-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.
+Lean4-Mode only supports version 4 of Lean.  For editing code written
+in deprecated version 3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as
+/Lean-Mode/ due to historical 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.  Make
+sure to not use these =lean-=-prefixed commands in buffers where
+Lean4-Mode is the major mode.
+
+* Contributing
+
+When you contribute to Lean4-Mode, add a personal copyright like =;;
+Copyright (c) 2024 Firstname Lastname= to the header of respective
+files.
+
+You can use Emacs' built-in ~bug-reference-mode~ and
+~bug-reference-prog-mode~ in this repository to make mentions of
+issues like =#123= clickable.
+
+* Changelog
+
+** Version 1.1.2
+
+- 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
+
+- 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
+
+- 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
+
+- Specify Yury G. Kudryashov as maintainer.
+- Rework README.  (Now in Org format).
+- Provide README as Texi and Info manual too.
+
+** Version 1.0
+
+- Specify "Version" in Emacs-Lisp library header.

lean4-eri.el

@@ -223,5 +223,24 @@ are calculated."
   (interactive)
   (lean4-eri-indent t))
 
+(defun lean4-eri-tab ()
+  "Lean4 function for TAB indent."
+  (interactive)
+  (if (looking-back (rx line-start (* white)) nil)
+      (lean4-eri-indent)
+    (let ((indent-line-function 'indent-relative))
+      (indent-for-tab-command))))
+
+(defun lean4-eri-init ()
+  "Setup buffer-local variables and minor modes for `lean4-eri'."
+  (setq-local indent-line-function
+              #'lean4-eri-tab)
+  (setq-local lisp-indent-function
+              #'common-lisp-indent-function)
+  (when (fboundp 'electric-indent-local-mode)
+      (electric-indent-local-mode -1))
+  (when (fboundp 'indent-tabs-mode)
+    (indent-tabs-mode -1)))
+
 (provide 'lean4-eri)
 ;;; lean4-eri.el ends here