Use "Lean4" in docstrings, for input method; name info "*Lean4 Info*"

README.org

@@ -143,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                           |

lean4-info.el

@@ -32,10 +32,9 @@
   "Lean4-Mode Info."
   :group 'lean4)
 
-;; Lean Info Mode (for "*lean4-info*" buffer)
 ;; Automode List
 ;;;###autoload
-(define-derived-mode lean4-info-mode prog-mode "Lean-Info"
+(define-derived-mode lean4-info-mode prog-mode "Lean4-Info"
   "Major mode for Lean4-Mode Info Buffer."
   :syntax-table lean4-syntax-table
   :group 'lean4
@@ -47,7 +46,7 @@
 
 (defun lean4-ensure-info-buffer (buffer)
   "Create BUFFER if it does not exist.
-Also choose settings used for the *Lean Goal* buffer."
+Also choose settings used for the *Lean4 Info* buffer."
   (unless (get-buffer buffer)
     (with-current-buffer (get-buffer-create buffer)
       (buffer-disable-undo)
@@ -57,7 +56,7 @@ Also choose settings used for the *Lean Goal* buffer."
 
 (defun lean4-toggle-info-buffer (buffer)
   "Create or delete BUFFER.
-The buffer is supposed to be the *Lean Goal* buffer."
+The buffer is supposed to be the *Lean4 Info* buffer."
   (-if-let (window (get-buffer-window buffer))
       (quit-window nil window)
     (lean4-ensure-info-buffer buffer)
@@ -79,7 +78,7 @@ The buffer is supposed to be the *Lean Goal* buffer."
     (:range :fullRange :message)
     (:code :relatedInformation :severity :source :tags))))
 
-(defconst lean4-info-buffer-name "*Lean Goal*")
+(defconst lean4-info-buffer-name "*Lean4 Info*")
 
 (defvar lean4-goals nil)
 (defvar lean4-term-goal nil)
@@ -233,7 +232,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
 
 
 (defcustom lean4-info-buffer-debounce-delay-sec 0.1
-  "Duration of time we wait before writing to *Lean Goal*."
+  "Duration of time we wait before writing to *Lean4 Info*."
   :group 'lean4-info
   :type 'number)
 
@@ -292,7 +291,7 @@ sections."
 
 
 (defun lean4-info-buffer-refresh ()
-  "Refresh the *Lean Goal* buffer."
+  "Refresh the *Lean4 Info* buffer."
   (when (lean4-info-buffer-active lean4-info-buffer-name)
     (lsp-request-async
      "$/lean/plainGoal"

lean4-input.el

@@ -22,7 +22,7 @@
 
 ;; A highly customisable input method which can inherit from other
 ;; Quail input methods.  By default the input method is geared towards
-;; the input of mathematical and other symbols in Lean programs.
+;; the input of mathematical and other symbols in Lean4 programs.
 
 ;; Use M-x customize-group lean4-input to customise this input method.
 ;; Note that the functions defined under "Functions used to tweak
@@ -145,7 +145,7 @@ This suffix is dropped."
 ;; until lean4-input-setup is called at the end of this file.
 
 (defgroup lean4-input nil
-  "The Lean input method.
+  "The Lean4 input method.
 After tweaking these settings you may want to inspect the resulting
 translations using `lean4-input-show-translations'."
   :group 'lean4
@@ -162,9 +162,9 @@ translations using `lean4-input-show-translations'."
                  (lean4-input-prefix "^"))
                 (lean4-input-prefix "_"))))))
   "List of parent Quail input methods.
-Translations from these methods will be inherited by the Lean
-input method (with the exception of translations corresponding to
-ASCII characters).
+Translations from these methods will be inherited by the Lean4 input
+method (with the exception of translations corresponding to ASCII
+characters).
 
 The list consists of pairs (qp . tweak), where qp is the name of
 a Quail package, and tweak is an expression of the same signature as
@@ -189,7 +189,7 @@ order for the change to take effect."
   :type 'directory)
 
 (defcustom lean4-input-user-translations nil
-  "A list of translations specific to the Lean input method.
+  "A list of translations specific to the Lean4 input method.
 Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).
 All the translation strings are possible translations
 of the given key sequence; if there is more than one you can choose
@@ -222,29 +222,29 @@ that contains all translations from QP Except for those corresponding to ASCII."
   "Display all translations used by the Quail package QP (a string).
 \(Except for those corresponding to ASCII)."
   (interactive (list (read-input-method-name
-                      "Quail input method (default %s): " "Lean")))
+                      "Quail input method (default %s): " "Lean4")))
   (let ((buf (concat "*" qp " input method translations*")))
     (with-output-to-temp-buffer buf
       (with-current-buffer buf
         (quail-insert-decode-map
          (cons 'decode-map (lean4-input-get-translations qp)))))))
 
 (defun lean4-input-add-translations (trans)
-  "Add the given translations TRANS to the Lean input method.
+  "Add the given translations TRANS to the Lean4 input method.
 TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION).  The
 translations are appended to the current translations."
   (with-temp-buffer
     (map-do (lambda (key tr)
               (when key
                 (quail-defrule (concat "\\" key)
                                tr
-                               "Lean" t)))
+                               "Lean4" t)))
             trans)))
 
 (defun lean4-input-inherit-package (qp &optional fun)
   "Inherit translations from the Quail package QP.
 Add all translations from the Quail package QP (except for those
-corresponding to ASCII) to the list of Lean Quail rules.
+corresponding to ASCII) to the list of Lean4 Quail rules.
 
 The optional function FUN can be used to modify the translations.
 It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return
@@ -261,14 +261,15 @@ a list of such pairs."
 (declare-function json-read "json")
 
 (defun lean4-input-setup ()
-  "Set up the Lean input method.
-Use customisable variables and parent input methods to setup Lean input method."
+  "Set up the Lean4 input method.
+Use customisable variables and parent input methods to setup Lean4 input
+method."
 
   ;; Create (or reset) the input method.
   (with-temp-buffer
-    (quail-define-package "Lean" "UTF-8" "∏" t ; guidance
-     "Lean input method.
-The purpose of this input method is to edit Lean programs, but
+    (quail-define-package "Lean4" "UTF-8" "∏" t ; guidance
+     "Lean4 input method.
+The purpose of this input method is to edit Lean4 programs, but
 since it is highly customisable it can be made useful for other
 tasks as well."
      nil nil nil nil nil nil t ; maximum-shortest
@@ -296,7 +297,7 @@ tasks as well."
                                 (eval (cdr def)))))
 
 (defun lean4-input-incorporate-changed-setting (sym val)
-  "Update the Lean input method.
+  "Update the Lean4 input method.
 Set SYM default value to VAL, then call `lean4-input-setup'.
 Suitable for use in the :set field of `defcustom'."
   (set-default sym val)

lean4-mode.info

@@ -229,7 +229,7 @@ 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 in
+will display the ‘*Lean4 Info*’ buffer (like the Lean Info-View pane in
 VS-Code) in a separate window.
 
 Key                      Description                                              Command

lean4-mode.texi

@@ -233,7 +233,7 @@ then type @samp{#check id}, the word @samp{#check} will be underlined, and
 hovering over it will show you the type of @code{id}.
 
 To view the proof state, run @code{lean4-toggle-info} (@samp{C-c C-i}).  This
-will display the @samp{*Lean Goals*} buffer (like the Lean Info-View pane
+will display the @samp{*Lean4 Info*} buffer (like the Lean Info-View pane
 in VS-Code) in a separate window.
 
 @multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa}