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 24, 2024 · 34366b3 · 34366b3
1 parent 801258f
commit 34366b3
Show file tree

Hide file tree

Showing 7 changed files with 125 additions and 117 deletions.
diff --git a/README.org b/README.org
@@ -23,8 +23,7 @@ known as /Lean-Mode/).
 Install dependencies:
 - [[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)
 
 Install Lean4-Mode:
@@ -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
@@ -30,7 +30,6 @@
 
 ;;; Code:
 
-(require 'dash)
 (require 'lean4-syntax)
 (require 'lean4-settings)
 (require 'lsp-mode)
@@ -67,7 +66,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 +141,35 @@ 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)
+  (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 +178,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
 Install dependencies:
    • 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 Instructions2565
-Node: Instructions for Source-Based Use-Package4119
-Node: Native vc (Emacs 30 or later)4840
-Node: Doom-Emacs5693
-Node: Straight6093
-Node: Usage6583
-Node: Key Bindings and Commands7503
+Node: Detailed and Concrete Instructions2463
+Node: Instructions for Source-Based Use-Package3838
+Node: Native vc (Emacs 30 or later)4559
+Node: Doom-Emacs5412
+Node: Straight5812
+Node: Usage6302
+Node: Key Bindings and Commands7222
 
 End Tag Table
 

diff --git a/lean4-mode.texi b/lean4-mode.texi
@@ -77,8 +77,7 @@ Install dependencies:
 @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)

diff --git a/lean4-syntax.el b/lean4-syntax.el
@@ -27,7 +27,6 @@
 
 ;;; Code:
 
-(require 'dash)
 (require 'rx)
 
 (defconst lean4-keywords1
@@ -86,53 +85,61 @@
     (modify-syntax-entry ?» ">" st)
 
     ;; Word constituent
-    (--each (list ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k ?l ?m
-                  ?n ?o ?p ?q ?r ?s ?t ?u ?v ?w ?x ?y ?z
-                  ?A ?B ?C ?D ?E ?F ?G ?H ?I ?J ?K ?L ?M
-                  ?N ?O ?P ?Q ?R ?S ?T ?U ?V ?W ?X ?Y ?Z)
-      (modify-syntax-entry it "w" st))
-    (--each (list ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9)
-      (modify-syntax-entry it "w" st))
-    (--each (list ?α ?β ?γ ?δ ?ε ?ζ ?η ?θ ?ι ?κ ;;?λ
-                  ?μ ?ν ?ξ ?ο ?π ?ρ ?ς ?σ ?τ ?υ
-                  ?φ ?χ ?ψ ?ω)
-      (modify-syntax-entry it "w" st))
-    (--each (list ?ϊ ?ϋ ?ό ?ύ ?ώ ?Ϗ ?ϐ ?ϑ ?ϒ ?ϓ ?ϔ ?ϕ ?ϖ
-                  ?ϗ ?Ϙ ?ϙ ?Ϛ ?ϛ ?Ϝ ?ϝ ?Ϟ ?ϟ ?Ϡ ?ϡ ?Ϣ ?ϣ
-                  ?Ϥ ?ϥ ?Ϧ ?ϧ ?Ϩ ?ϩ ?Ϫ ?ϫ ?Ϭ ?ϭ ?Ϯ ?ϯ ?ϰ
-                  ?ϱ ?ϲ ?ϳ ?ϴ ?ϵ ?϶ ?Ϸ ?ϸ ?Ϲ ?Ϻ ?ϻ)
-      (modify-syntax-entry it "w" st))
-    (--each (list ?ἀ ?ἁ ?ἂ ?ἃ ?ἄ ?ἅ ?ἆ ?ἇ ?Ἀ ?Ἁ ?Ἂ ?Ἃ ?Ἄ
-                  ?Ἅ ?Ἆ ?Ἇ ?ἐ ?ἑ ?ἒ ?ἓ ?ἔ ?ἕ ?἖ ?἗ ?Ἐ ?Ἑ
-                  ?Ἒ ?Ἓ ?Ἔ ?Ἕ ?἞ ?἟ ?ἠ ?ἡ ?ἢ ?ἣ ?ἤ ?ἥ
-                  ?ἦ ?ἧ ?Ἠ ?Ἡ ?Ἢ ?Ἣ ?Ἤ ?Ἥ ?Ἦ ?Ἧ ?ἰ ?ἱ
-                  ?ἲ ?ἳ ?ἴ ?ἵ ?ἶ ?ἷ ?Ἰ ?Ἱ ?Ἲ ?Ἳ ?Ἴ ?Ἵ ?Ἶ ?Ἷ
-                  ?ὀ ?ὁ ?ὂ ?ὃ ?ὄ ?ὅ ?὆ ?὇ ?Ὀ ?Ὁ ?Ὂ ?Ὃ
-                  ?Ὄ ?Ὅ ?὎ ?὏ ?ὐ ?ὑ ?ὒ ?ὓ ?ὔ ?ὕ ?ὖ ?ὗ
-                  ?὘ ?Ὑ ?὚ ?Ὓ ?὜ ?Ὕ ?὞ ?Ὗ ?ὠ ?ὡ ?ὢ
-                  ?ὣ ?ὤ ?ὥ ?ὦ ?ὧ ?Ὠ ?Ὡ ?Ὢ ?Ὣ ?Ὤ ?Ὥ ?Ὦ
-                  ?Ὧ ?ὰ ?ά ?ὲ ?έ ?ὴ ?ή ?ὶ ?ί ?ὸ ?ό ?ὺ ?ύ ?ὼ
-                  ?ώ ?὾ ?὿ ?ᾀ ?ᾁ ?ᾂ ?ᾃ ?ᾄ ?ᾅ ?ᾆ ?ᾇ ?ᾈ
-                  ?ᾉ ?ᾊ ?ᾋ ?ᾌ ?ᾍ ?ᾎ ?ᾏ ?ᾐ ?ᾑ ?ᾒ ?ᾓ ?ᾔ
-                  ?ᾕ ?ᾖ ?ᾗ ?ᾘ ?ᾙ ?ᾚ ?ᾛ ?ᾜ ?ᾝ ?ᾞ ?ᾟ ?ᾠ ?ᾡ ?ᾢ
-                  ?ᾣ ?ᾤ ?ᾥ ?ᾦ ?ᾧ ?ᾨ ?ᾩ ?ᾪ ?ᾫ ?ᾬ ?ᾭ ?ᾮ ?ᾯ ?ᾰ
-                  ?ᾱ ?ᾲ ?ᾳ ?ᾴ ?᾵ ?ᾶ ?ᾷ ?Ᾰ ?Ᾱ ?Ὰ ?Ά ?ᾼ ?᾽
-                  ?ι ?᾿ ?῀ ?῁ ?ῂ ?ῃ ?ῄ ?῅ ?ῆ ?ῇ ?Ὲ ?Έ ?Ὴ
-                  ?Ή ?ῌ ?῍ ?῎ ?῏ ?ῐ ?ῑ ?ῒ ?ΐ ?῔ ?῕ ?ῖ ?ῗ
-                  ?Ῐ ?Ῑ ?Ὶ ?Ί ?῜ ?῝ ?῞ ?῟ ?ῠ ?ῡ ?ῢ ?ΰ ?ῤ ?ῥ
-                  ?ῦ ?ῧ ?Ῠ ?Ῡ ?Ὺ ?Ύ ?Ῥ ?῭ ?΅ ?` ?῰ ?῱ ?ῲ ?ῳ
-                  ?ῴ ?῵ ?ῶ ?ῷ ?Ὸ ?Ό ?Ὼ ?Ώ ?ῼ ?´ ?῾)
-      (modify-syntax-entry it "w" st))
-    (--each (list ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ
-                  ?ℏ ?ℐ ?ℑ ?ℒ ?ℓ ?℔ ?ℕ ?№ ?℗ ?℘ ?ℙ ?ℚ ?ℛ ?ℜ ?ℝ
-                  ?℞ ?℟ ?℠ ?℡ ?™ ?℣ ?ℤ ?℥ ?Ω ?℧ ?ℨ ?℩ ?K ?Å ?ℬ
-                  ?ℭ ?℮ ?ℯ ?ℰ ?ℱ ?Ⅎ ?ℳ ?ℴ ?ℵ ?ℶ ?ℷ ?ℸ ?ℹ ?℺ ?℻
-                  ?ℼ ?ℽ ?ℾ ?ℿ ?⅀ ?⅁ ?⅂ ?⅃ ?⅄ ?ⅅ ?ⅆ ?ⅇ ?ⅈ ?ⅉ ?⅊
-                  ?⅋ ?⅌ ?⅍ ?ⅎ ?⅏)
-      (modify-syntax-entry it "w" st))
-    (--each (list ?₁ ?₂ ?₃ ?₄ ?₅ ?₆ ?₇ ?₈ ?₉ ?₀
+    (dolist (it '(;; Punctuation
+                  ?! ?'
+                  ;; Digits
+                  ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9
+                  ;; Punctuation
+                  ??
+                  ;; Latin capital letters
+                  ?A ?B ?C ?D ?E ?F ?G ?H ?I ?J ?K ?L ?M ?N ?O ?P ?Q
+                  ?R ?S ?T ?U ?V ?W ?X ?Y ?Z
+                  ;; Punctuation
+                  ?_
+                  ;; Latin small letters
+                  ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k ?l ?m ?n ?o ?p ?q
+                  ?r ?s ?t ?u ?v ?w ?x ?y ?z
+                  ;; Greek small letters
+                  ?α ?β ?γ ?δ ?ε ?ζ ?η ?θ ?ι ?κ ;; No ?λ!
+                  ?μ ?ν ?ξ ?ο ?π ?ρ ?ς ?σ ?τ ?υ ?φ ?χ ?ψ ?ω
+                  ;; Greek small letters with diacritics
+                  ?ϊ ?ϋ ?ό ?ύ ?ώ ?Ϗ ?ϐ ?ϑ ?ϒ ?ϓ ?ϔ
+                  ;; Greek letter symbols
+                  ?ϕ ?ϖ ?ϗ
+                  ;; Greek archaic letters
+                  ?Ϙ ?ϙ
+                  ;; Greek rare letters
+                  ?Ϛ ?ϛ ?Ϝ ?ϝ ?Ϟ ?ϟ ?Ϡ ?ϡ
+                  ;; Coptic letters
+                  ?Ϣ ?ϣ ?Ϥ ?ϥ ?Ϧ ?ϧ ?Ϩ ?ϩ ?Ϫ ?ϫ ?Ϭ ?ϭ ?Ϯ ?ϯ
+                  ;; Greek
+                  ?ϰ ?ϱ ?ϲ ?ϳ ?ϴ ?ϵ ?϶ ?Ϸ ?ϸ ?Ϲ ?Ϻ ?ϻ
+                  ;; Greek letters and diacritics
+                  ?ἀ ?ἁ ?ἂ ?ἃ ?ἄ ?ἅ ?ἆ ?ἇ ?Ἀ ?Ἁ ?Ἂ ?Ἃ ?Ἄ ?Ἅ ?Ἆ ?Ἇ ?ἐ
+                  ?ἑ ?ἒ ?ἓ ?ἔ ?ἕ ?἖ ?἗ ?Ἐ ?Ἑ ?Ἒ ?Ἓ ?Ἔ ?Ἕ ?἞ ?἟ ?ἠ ?ἡ
+                  ?ἢ ?ἣ ?ἤ ?ἥ ?ἦ ?ἧ ?Ἠ ?Ἡ ?Ἢ ?Ἣ ?Ἤ ?Ἥ ?Ἦ ?Ἧ ?ἰ ?ἱ ?ἲ
+                  ?ἳ ?ἴ ?ἵ ?ἶ ?ἷ ?Ἰ ?Ἱ ?Ἲ ?Ἳ ?Ἴ ?Ἵ ?Ἶ ?Ἷ ?ὀ ?ὁ ?ὂ ?ὃ
+                  ?ὄ ?ὅ ?὆ ?὇ ?Ὀ ?Ὁ ?Ὂ ?Ὃ ?Ὄ ?Ὅ ?὎ ?὏ ?ὐ ?ὑ ?ὒ ?ὓ ?ὔ
+                  ?ὕ ?ὖ ?ὗ ?὘ ?Ὑ ?὚ ?Ὓ ?὜ ?Ὕ ?὞ ?Ὗ ?ὠ ?ὡ ?ὢ ?ὣ ?ὤ ?ὥ
+                  ?ὦ ?ὧ ?Ὠ ?Ὡ ?Ὢ ?Ὣ ?Ὤ ?Ὥ ?Ὦ ?Ὧ ?ὰ ?ά ?ὲ ?έ ?ὴ ?ή ?ὶ
+                  ?ί ?ὸ ?ό ?ὺ ?ύ ?ὼ ?ώ ?὾ ?὿ ?ᾀ ?ᾁ ?ᾂ ?ᾃ ?ᾄ ?ᾅ ?ᾆ ?ᾇ
+                  ?ᾈ ?ᾉ ?ᾊ ?ᾋ ?ᾌ ?ᾍ ?ᾎ ?ᾏ ?ᾐ ?ᾑ ?ᾒ ?ᾓ ?ᾔ ?ᾕ ?ᾖ ?ᾗ ?ᾘ
+                  ?ᾙ ?ᾚ ?ᾛ ?ᾜ ?ᾝ ?ᾞ ?ᾟ ?ᾠ ?ᾡ ?ᾢ ?ᾣ ?ᾤ ?ᾥ ?ᾦ ?ᾧ ?ᾨ ?ᾩ
+                  ?ᾪ ?ᾫ ?ᾬ ?ᾭ ?ᾮ ?ᾯ ?ᾰ ?ᾱ ?ᾲ ?ᾳ ?ᾴ ?᾵ ?ᾶ ?ᾷ ?Ᾰ ?Ᾱ ?Ὰ
+                  ?Ά ?ᾼ ?᾽ ?ι ?᾿ ?῀ ?῁ ?ῂ ?ῃ ?ῄ ?῅ ?ῆ ?ῇ ?Ὲ ?Έ ?Ὴ ?Ή
+                  ?ῌ ?῍ ?῎ ?῏ ?ῐ ?ῑ ?ῒ ?ΐ ?῔ ?῕ ?ῖ ?ῗ ?Ῐ ?Ῑ ?Ὶ ?Ί ?῜
+                  ?῝ ?῞ ?῟ ?ῠ ?ῡ ?ῢ ?ΰ ?ῤ ?ῥ ?ῦ ?ῧ ?Ῠ ?Ῡ ?Ὺ ?Ύ ?Ῥ ?῭
+                  ?΅ ?` ?῰ ?῱ ?ῲ ?ῳ ?ῴ ?῵ ?ῶ ?ῷ ?Ὸ ?Ό ?Ὼ ?Ώ ?ῼ ?´ ?῾
+                  ;; Subscript digits
+                  ?₀ ?₁ ?₂ ?₃ ?₄ ?₅ ?₆ ?₇ ?₈ ?₉
+                  ;; Subscript letters
                   ?ₐ ?ₑ ?ₒ ?ₓ ?ₔ ?ₕ ?ₖ ?ₗ ?ₘ ?ₙ ?ₚ ?ₛ ?ₜ
-                  ?' ?_ ?! ??)
+                  ;; Various
+                  ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ ?ℏ ?ℐ
+                  ?ℑ ?ℒ ?ℓ ?℔ ?ℕ ?№ ?℗ ?℘ ?ℙ ?ℚ ?ℛ ?ℜ ?ℝ ?℞ ?℟ ?℠ ?℡
+                  ?™ ?℣ ?ℤ ?℥ ?Ω ?℧ ?ℨ ?℩ ?K ?Å ?ℬ ?ℭ ?℮ ?ℯ ?ℰ ?ℱ ?Ⅎ
+                  ?ℳ ?ℴ ?ℵ ?ℶ ?ℷ ?ℸ ?ℹ ?℺ ?℻ ?ℼ ?ℽ ?ℾ ?ℿ ?⅀ ?⅁ ?⅂ ?⅃
+                  ?⅄ ?ⅅ ?ⅆ ?ⅇ ?ⅈ ?ⅉ ?⅊ ?⅋ ?⅌ ?⅍ ?ⅎ ?⅏))
       (modify-syntax-entry it "w" st))
 
     ;; Lean operator chars
@@ -217,7 +224,7 @@
            (,(rx line-start "No Goal" line-end)
             . 'font-lock-constant-face)))
         (inherited-entries (car lean4-font-lock-defaults)))
-    `(,(-concat new-entries inherited-entries))))
+    `(,(append new-entries inherited-entries))))
 
 (provide 'lean4-syntax)
 ;;; lean4-syntax.el ends here