[elpa] externals/eev 7642c0f5fc: Made (find-lean4-intro) work with Emacs28.

[ELPA Syncer]

branch: externals/eev
commit 7642c0f5fc40212cb88961c97f134cf839d37683
Author: Eduardo Ochs <eduardoochs@gmail.com>
Commit: Eduardo Ochs <eduardoochs@gmail.com>

    Made (find-lean4-intro) work with Emacs28.
---
 ChangeLog     |  6 ++++++
 VERSION       |  4 ++--
 eev-intro.el  | 68 +++++++++++++++++++++++++++++++++++++++++++++++++----------
 eev-lean4.el  | 11 +++++++---
 eev-tlinks.el |  5 ++++-
 5 files changed, 77 insertions(+), 17 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 4de12e3d8d..0ab0a80009 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2024-07-29  Eduardo Ochs  <eduardoochs@gmail.com>
+
+       * eev-intro.el (find-emacs-keys-intro): list some key sequences
+       for frames.
+       (find-lean4-intro): many changes; made it work on Emacs28.
+
 2024-07-26  Eduardo Ochs  <eduardoochs@gmail.com>
 
        * eev-tlinks.el (ee-dot-emacs-eevgit): new function.
diff --git a/VERSION b/VERSION
index bb452b0c12..f127fcc4a0 100644
--- a/VERSION
+++ b/VERSION
@@ -1,2 +1,2 @@
-Sat Jul 27 00:17:49 GMT 2024
-Fri Jul 26 21:17:49 -03 2024
+Mon Jul 29 04:03:07 GMT 2024
+Mon Jul 29 01:03:07 -03 2024
diff --git a/eev-intro.el b/eev-intro.el
index 21c32589f7..5245ecf583 100644
--- a/eev-intro.el
+++ b/eev-intro.el
@@ -19,7 +19,7 @@
 ;;
 ;; Author:     Eduardo Ochs <eduardoochs@gmail.com>
 ;; Maintainer: Eduardo Ochs <eduardoochs@gmail.com>
-;; Version:    20240726
+;; Version:    20240729
 ;; Keywords:   e-scripts
 ;;
 ;; Latest version: <http://anggtwu.net/eev-current/eev-intro.el>
@@ -2135,6 +2135,10 @@ C-x 2   -- split-window-vertically (Above/Below) 
(find-enode \"Split Window\")
 C-x 3   -- split-window-horizontally       (L|R) (find-enode \"Split Window\")
 C-x 4 0 -- kill-buffer-and-window                (find-enode \"Change Window\")
 C-x +   -- balance-windows                       (find-enode \"Change Window\")
+C-x 5 o        -- other-frame                           (find-enode \"Frame 
Commands\")
+C-x 5 0 -- delete-frame                          (find-enode \"Frame 
Commands\")
+C-x 5 1 -- delete-other-frames                   (find-enode \"Frame 
Commands\")
+C-x 5 2        -- make-frame-command                    (find-enode \"Creating 
Frames\")
 
 
 
@@ -17931,12 +17935,16 @@ i.e.,:
   rm -Rv /tmp/elan-install/
   mkdir  /tmp/elan-install/
   cd     /tmp/elan-install/
-  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh 
-sSf \
-    | sh -s -- --default-toolchain leanprover/lean4:stable
+  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh 
-sSf \\
+    | sh -s -- -y --default-toolchain leanprover/lean4:stable
 
-The installer will ask if you want it to change some files like
-~/.bashrc and ~/.zshrc to include ~/.elan/bin/ in the PATH. If you're
-only going to use Lean from Emacs, say no - because of this:
+The \"-y\" after the \"sh\" in the last line makes the installer use
+certain defaults without asking questions.
+
+Note about $PATH: if you remove the \"-y\" then the installer may ask if
+you want it to change some files like ~/.bashrc and ~/.zshrc to include
+~/.elan/bin/ in the PATH. If you're only going to use Lean from Emacs,
+you can say no - because of this:
 
   (find-eev \"eev-lean4.el\" \"PATH\")
 
@@ -17979,13 +17987,32 @@ then run this progn,
 
   (progn
     (find-2a nil '(find-ebuffer \"*Messages*\"))
+    (add-to-list 'package-archives
+      '(\"melpa\" . \"https://melpa.org/packages/\";))
+    ;;
+    (setq package-check-signature nil)
+    ;;
     (package-initialize)
     (package-refresh-contents)
+    ;;
+    ;; Make everything work on Emacs28:
+    (setq package-install-upgrade-built-in t)
+    (package-install 'gnu-elpa-keyring-update)
+    (package-install 'compat)
+    (package-install 'seq)
+    (progn (unload-feature 'seq t) (require 'seq))
+    (package-install 'magit)
+    ;;
+    (setq package-check-signature nil)
+    ;;
+    ;; Missing in the instructions for lean4-mode:
+    (package-install 'company)
+    ;;
+    ;; From the instructions for lean4-mode:
     (package-install 'dash)
     (package-install 'flycheck)
     (package-install 'lsp-mode)
     (package-install 'magit-section)
-    (package-install 'company)
     )
 
 and try:
@@ -18005,7 +18032,7 @@ If you open the file Init.lean with the second sexp 
below,
   (find-lean4prefile \"Init.lean\")
 
 then lsp-mode will ask where is the \"project root\", and there will be
-an option to say that it is at that the directory above, i.e., at:
+an option (\"i\") to say that it is at the directory above, i.e., at:
 
   ~/.elan/toolchains/leanprover--lean4---stable/
 
@@ -18023,15 +18050,34 @@ Try this with `M-3 M-e':
 the prefix `M-3' will make the file be opened at the window at the
 right. Then try these navigation keys:
 
-  M-.   - go forward (xref-find-definitions)
+  M-.   - go to   (xref-find-definitions)
   M-,   - go back (xref-go-back)
 
+For a demo of these keys, see this part of the video (in Portuguese):
+
+  (find-2024lean4of0hsubs \"14:12\" \"`go to' e `go back'\")
+  (find-2024lean4of0video \"14:12\" \"`go to' e `go back'\")
+
+
 
 
 9. Try a snippet
 ================
-In: (find-es \"lean\" \"Std.Format\")
-TODO: explain this!
+Watch this part of the video,
+
+  (find-2024lean4of0hsubs \"16:31\" \"(anotações sobre coerção)\")
+  (find-2024lean4of0video \"16:31\" \"(anotações sobre coerção)\")
+  (find-2024lean4of0hsubs \"17:39\" \"bota isso aqui no clipboard do Emacs\")
+  (find-2024lean4of0video \"17:39\" \"bota isso aqui no clipboard do Emacs\")
+
+and try to use the notes in the link below, including the snippet.
+If LSP asks for a project root, answer \"i\", for:
+
+  i ==> Import project root /tmp/L/
+
+Here is the link:
+
+  (find-es \"lean\" \"Std.Format\")
 
 
 
diff --git a/eev-lean4.el b/eev-lean4.el
index 6aae421a8b..2c824f1119 100644
--- a/eev-lean4.el
+++ b/eev-lean4.el
@@ -19,7 +19,7 @@
 ;;
 ;; Author:     Eduardo Ochs <eduardoochs@gmail.com>
 ;; Maintainer: Eduardo Ochs <eduardoochs@gmail.com>
-;; Version:    20240726
+;; Version:    20240728
 ;; Keywords:   e-scripts
 ;;
 ;; Latest version: <http://anggtwu.net/eev-current/eev-lean4.el>
@@ -36,6 +36,7 @@
 ;;   (find-lean4-intro)
 ;;
 ;; This is very experimental and very undocumented!
+;; Reload with:
 ;;
 ;;   (load (buffer-file-name))
 
@@ -60,6 +61,10 @@
 ;;   «.ee-leandoc-:tclean4»    (to "ee-leandoc-:tclean4")
 ;;   «.ee-leandoc-:tpil4»      (to "ee-leandoc-:tpil4")
 
+;; (require 'subr-x)
+(require 'eev-rstdoc)
+(setq package-install-upgrade-built-in t) ; needed for Emacs28?
+
 
 
 
@@ -70,8 +75,8 @@
 ;;; |_| /_/   \_\_| |_| |_|
 ;;;                        
 ;; «PATH»  (to ".PATH")
-;; See: (find-es "lean" "install-2024")
-;; export PATH=$HOME/.elan/bin:$PATH
+;; Similar to: export PATH=$HOME/.elan/bin:$PATH
+;;        See: (find-lean4-intro "4. Install Lean4")
 (setenv "PATH" (format "%s/.elan/bin:%s" (getenv "HOME") (getenv "PATH")))
 ;; (find-sh "echo $PATH")
 ;; (find-sh "echo $PATH | tr : '\n'")
diff --git a/eev-tlinks.el b/eev-tlinks.el
index a55c1f1b6e..9742931c03 100644
--- a/eev-tlinks.el
+++ b/eev-tlinks.el
@@ -198,6 +198,7 @@
 (require 'eev-env)
 (require 'eev-wrap)    ; For: (find-eev "eev-wrap.el" "ee-template0") 
 (require 'cl-lib)      ; For `cl-remove-if'
+(require 'subr-x)      ; For `string-join'
 
 
 
@@ -3240,7 +3241,9 @@ call BINARY instead of \"google-chrome\"."
      ""
      ,(ee-template0 "\
 ;; Make `{binary}' the default browser.
-;; This is a hack that makes `find-googlechrome' call `{binary}'!
+;; This is a hack that makes `find-googlechrome' call `{binary}'.
+;; Note that this hack bypasses the variable `ee-googlechrome-program'!
+;; See: (find-eev \"eev-plinks.el\" \"find-googlechrome\")
 
 
 ;; Try: