Do not depend on Dash

Fixes #68 "Don't depend on Dash" (<#68>). In README, do not mention Dash. Most complex change involves a replacement for an expression like (-let* (((a b) (--split-with ...)))) for which a new (private inline helper) function has been introduced: lean4-info-buffer-redisplay--partition-errors.
leanprover-community · Nov 26, 2024 · b4c3007 · b4c3007
1 parent b5627b0
commit b4c3007
Show file tree

Hide file tree

Showing 7 changed files with 135 additions and 119 deletions.
diff --git a/README.org b/README.org
@@ -23,8 +23,7 @@ known as /Lean-Mode/).
 First, install the dependencies of Lean4-Mode:
 - [[https://lean-lang.org/lean4/doc/setup.html][Lean version 4]]
 - Emacs version 27 or later
-- Emacs packages [[https://github.com/magnars/dash.el][Dash]] (which is available on GNU-Elpa
-  package-archive), [[https://www.flycheck.org][Flycheck]], [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]], and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (which are
+- Emacs packages [[https://www.flycheck.org][Flycheck]], [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]], and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (which are
   available on Melpa package-archive)
 
 Second, install Lean4-Mode itself:
@@ -40,11 +39,9 @@ Install Lean version 4.
 
 Install Emacs version 27 or later.
 
-Install the Emacs packages Dash, Flycheck, lsp-mode and Magit-Section.
-Dash is the only one of these packages that is available in the
-default [[https://elpa.gnu.org][GNU Elpa]] package-archive.  You can install the remaining three
-packages either from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive.  For later
-approach, add the following to your Emacs initialization file
+Install the Emacs packages Flycheck, lsp-mode and Magit-Section either
+from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive.  For later approach, add
+the following to your Emacs initialization file
 (e.g. =~/.emacs.d/init.el=):
 
 #+begin_src elisp
@@ -53,7 +50,7 @@ approach, add the following to your Emacs initialization file
              '("melpa" . "https://melpa.org/packages/"))
 (package-initialize)
 (let ((need-to-refresh t))
-  (dolist (package '(dash flycheck lsp-mode magit-section))
+  (dolist (package '(flycheck lsp-mode magit-section))
     (unless (package-installed-p package)
       (when need-to-refresh
         (package-refresh-contents)

diff --git a/lean4-info.el b/lean4-info.el
@@ -1,7 +1,8 @@
 ;;; lean4-info.el --- Emacs mode for Lean theorem prover -*- lexical-binding: t -*-
-;;
+
 ;; Copyright (c) 2016 Gabriel Ebner. All rights reserved.
-;;
+;; Copyright (c) 2024 Mekeor Melire
+
 ;; Author: Gabriel Ebner <[email protected]>
 ;; Maintainer: Gabriel Ebner <[email protected]>
 ;; Created: Oct 29, 2016
@@ -30,7 +31,6 @@
 
 ;;; Code:
 
-(require 'dash)
 (require 'lean4-syntax)
 (require 'lean4-settings)
 (require 'lsp-mode)
@@ -67,7 +67,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."
-  (-if-let (window (get-buffer-window buffer))
+  (if-let ((window (get-buffer-window buffer)))
       (quit-window nil window)
     (lean4-ensure-info-buffer buffer)
     (display-buffer buffer)))
@@ -142,18 +142,42 @@ The buffer is supposed to be the *Lean Goal* buffer."
                                   'help-echo "mouse-2: visit this file, line and column"))
             (lean4-info--insert-highlight-inaccessible-names "\n" message "\n")))))))
 
+(define-inline lean4-info-buffer-redisplay--partition-errors (line errors)
+  "Partition ERRORS into errors above, on and below LINE.
+
+It is assumed that the ERRORS list is sorted ascendingly on the
+`lean4-diagnostic-full-end-line' predicate.  The result is a list with
+three elements: Firstly, the errors above the given LINE; secondly, the
+errors on given LINE; and thirdly, the errors below given LINE."
+  (let* ((above nil)
+         (here nil)
+         (below (seq-drop-while
+                 (lambda (e)
+                   (when (= (lean4-diagnostic-full-end-line e) line)
+                     (push e here)))
+                 (seq-drop-while
+                  (lambda (e)
+                    (when (< (lean4-diagnostic-full-end-line e) line)
+                      (push e above)))
+                  errors))))
+    (nreverse above)
+    (nreverse here)
+    (list above here below)))
+
 (defun lean4-info-buffer-redisplay ()
   (when (lean4-info-buffer-active lean4-info-buffer-name)
-    (-let* ((deactivate-mark) ; keep transient mark
-            (inhibit-read-only t)
-            (buffer (current-buffer))
-            (line (lsp--cur-line))
-            (errors (lsp--get-buffer-diagnostics))
-            (errors (-sort (-on #'< #'lean4-diagnostic-full-end-line) errors))
-            ((errors-above errors)
-             (--split-with (< (lean4-diagnostic-full-end-line it) line) errors))
-            ((errors-here errors-below)
-             (--split-with (<= (lean4-diagnostic-full-start-line it) line) errors)))
+    (let* ((deactivate-mark) ; keep transient mark
+           (inhibit-read-only t)
+           (buffer (current-buffer))
+           (line (lsp--cur-line))
+           (errors (lsp--get-buffer-diagnostics))
+           (errors (seq-sort-by
+                    #'lean4-diagnostic-full-end-line #'< errors))
+           (errors (lean4-info-buffer-redisplay--partition-errors
+                    line errors))
+           (errors-above (nth 0 errors))
+           (errors-here (nth 1 errors))
+           (errors-below (nth 2 errors)))
       (with-current-buffer lean4-info-buffer-name
         (progn
           (erase-buffer)
@@ -162,11 +186,11 @@ The buffer is supposed to be the *Lean Goal* buffer."
               (magit-insert-section (magit-section 'goals)
                 (magit-insert-heading "Goals:")
                 (magit-insert-section-body
-                (if (> (length goals) 0)
-                    (seq-doseq (g goals)
-                      (magit-insert-section (magit-section)
-                        (lean4--insert-goal-text g "\n\n")))
-                  (insert "goals accomplished\n\n")))))
+                  (if (> (length goals) 0)
+                      (seq-doseq (g goals)
+                        (magit-insert-section (magit-section)
+                          (lean4--insert-goal-text g "\n\n")))
+                    (insert "goals accomplished\n\n")))))
             (when-let ((term-goal lean4-term-goal)) ;; capture for deferred rendering
               (magit-insert-section (magit-section 'term-goal)
                 (magit-insert-heading "Expected type:")

diff --git a/lean4-input.el b/lean4-input.el
@@ -40,7 +40,6 @@
 (require 'quail)
 (require 'cl-lib)
 (require 'subr-x)
-(require 'dash)
 (require 'map)
 
 ;; Quail is quite stateful, so be careful when editing this code.  Note
@@ -317,21 +316,19 @@ 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 "};"))))
+  (with-current-buffer (get-buffer-create "*lean4-translations*")
+    (insert "var corrections = {")
+    (dolist (translation
+             (seq-difference (lean4-input-get-translations "Lean")
+                             '("\\newline")))
+      (let* ((input (substring (car translation) 1))
+             (outputs (cdr translation)))
+        (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."

diff --git a/lean4-mode.el b/lean4-mode.el
@@ -10,7 +10,7 @@
 ;; Maintainer: Yury G. Kudryashov <[email protected]>
 ;; Created: Jan 09, 2014
 ;; Keywords: languages
-;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0"))
+;; Package-Requires: ((emacs "27.1") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0"))
 ;; URL: https://github.com/leanprover/lean4-mode
 ;; SPDX-License-Identifier: Apache-2.0
 ;; Version: 1.0.1
@@ -42,7 +42,6 @@
 ;;; Code:
 
 (require 'cl-lib)
-(require 'dash)
 (require 'pcase)
 (require 'flycheck)
 (require 'lsp-mode)

diff --git a/lean4-mode.info b/lean4-mode.info
@@ -69,9 +69,7 @@ File: lean4-mode.info,  Node: Brief and Generic Instructions,  Next: Detailed an
 First, install the dependencies of Lean4-Mode:
    • Lean version 4 (https://lean-lang.org/lean4/doc/setup.html)
    • Emacs version 27 or later
-   • Emacs packages Dash (https://github.com/magnars/dash.el) (which is
-     available on GNU-Elpa package-archive), Flycheck
-     (https://www.flycheck.org), lsp-mode
+   • Emacs packages Flycheck (https://www.flycheck.org), lsp-mode
      (https://emacs-lsp.github.io/lsp-mode), and Magit-Section
      (https://github.com/magit/magit/blob/main/lisp/magit-section.el)
      (which are available on Melpa package-archive)
@@ -93,20 +91,17 @@ Install Lean version 4.
 
    Install Emacs version 27 or later.
 
-   Install the Emacs packages Dash, Flycheck, lsp-mode and
-Magit-Section.  Dash is the only one of these packages that is available
-in the default GNU Elpa (https://elpa.gnu.org) package-archive.  You can
-install the remaining three packages either from source or from Melpa
-(https://melpa.org/#/getting-started) package-archive.  For later
-approach, add the following to your Emacs initialization file (e.g.
-‘~/.emacs.d/init.el’):
+   Install the Emacs packages Flycheck, lsp-mode and Magit-Section
+either from source or from Melpa (https://melpa.org/#/getting-started)
+package-archive.  For later approach, add the following to your Emacs
+initialization file (e.g.  ‘~/.emacs.d/init.el’):
 
      (require 'package)
      (add-to-list 'package-archives
                   '("melpa" . "https://melpa.org/packages/"))
      (package-initialize)
      (let ((need-to-refresh t))
-       (dolist (package '(dash flycheck lsp-mode magit-section))
+       (dolist (package '(flycheck lsp-mode magit-section))
          (unless (package-installed-p package)
            (when need-to-refresh
              (package-refresh-contents)
@@ -248,13 +243,13 @@ Tag Table:
 Node: Top223
 Node: Installation1324
 Node: Brief and Generic Instructions1567
-Node: Detailed and Concrete Instructions2605
-Node: Instructions for Source-Based Use-Package4159
-Node: Native vc (Emacs 30 or later)4880
-Node: Doom-Emacs5733
-Node: Straight6133
-Node: Usage6623
-Node: Key Bindings and Commands7543
+Node: Detailed and Concrete Instructions2503
+Node: Instructions for Source-Based Use-Package3878
+Node: Native vc (Emacs 30 or later)4599
+Node: Doom-Emacs5452
+Node: Straight5852
+Node: Usage6342
+Node: Key Bindings and Commands7262
 
 End Tag Table
 

diff --git a/lean4-mode.texi b/lean4-mode.texi
@@ -77,8 +77,7 @@ First, install the dependencies of Lean4-Mode:
 @item
 Emacs version 27 or later
 @item
-Emacs packages @uref{https://github.com/magnars/dash.el, Dash} (which is available on GNU-Elpa
-package-archive), @uref{https://www.flycheck.org, Flycheck}, @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode}, and @uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (which are
+Emacs packages @uref{https://www.flycheck.org, Flycheck}, @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode}, and @uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (which are
 available on Melpa package-archive)
 @end itemize
 
@@ -98,11 +97,9 @@ Install Lean version 4.
 
 Install Emacs version 27 or later.
 
-Install the Emacs packages Dash, Flycheck, lsp-mode and Magit-Section.
-Dash is the only one of these packages that is available in the
-default @uref{https://elpa.gnu.org, GNU Elpa} package-archive.  You can install the remaining three
-packages either from source or from @uref{https://melpa.org/#/getting-started, Melpa} package-archive.  For later
-approach, add the following to your Emacs initialization file
+Install the Emacs packages Flycheck, lsp-mode and Magit-Section either
+from source or from @uref{https://melpa.org/#/getting-started, Melpa} package-archive.  For later approach, add
+the following to your Emacs initialization file
 (e.g. @samp{~/.emacs.d/init.el}):
 
 @lisp
@@ -111,7 +108,7 @@ approach, add the following to your Emacs initialization file
              '("melpa" . "https://melpa.org/packages/"))
 (package-initialize)
 (let ((need-to-refresh t))
-  (dolist (package '(dash flycheck lsp-mode magit-section))
+  (dolist (package '(flycheck lsp-mode magit-section))
     (unless (package-installed-p package)
       (when need-to-refresh
         (package-refresh-contents)