diff --git a/README.org b/README.org index 67f6c42..9ed4a75 100644 --- 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 index 5d6817f..5c9d17f 100644 --- 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 index 040e7f7..2698505 100644 --- 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 index fb52fa5..f1759b4 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -10,7 +10,7 @@ ;; Maintainer: Yury G. Kudryashov ;; 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 index c36d086..e43e057 100644 --- 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 index 4efbaf2..4837b52 100644 --- 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) diff --git a/lean4-syntax.el b/lean4-syntax.el index 39b41b0..4963565 100644 --- 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 ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ - ?ℏ ?ℐ ?ℑ ?ℒ ?ℓ ?℔ ?ℕ ?№ ?℗ ?℘ ?ℙ ?ℚ ?ℛ ?ℜ ?ℝ - ?℞ ?℟ ?℠ ?℡ ?™ ?℣ ?ℤ ?℥ ?Ω ?℧ ?ℨ ?℩ ?K ?Å ?ℬ - ?ℭ ?℮ ?ℯ ?ℰ ?ℱ ?Ⅎ ?ℳ ?ℴ ?ℵ ?ℶ ?ℷ ?ℸ ?ℹ ?℺ ?℻ - ?ℼ ?ℽ ?ℾ ?ℿ ?⅀ ?⅁ ?⅂ ?⅃ ?⅄ ?ⅅ ?ⅆ ?ⅇ ?ⅈ ?ⅉ ?⅊ - ?⅋ ?⅌ ?⅍ ?ⅎ ?⅏) - (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 + ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ ?ℏ ?ℐ + ?ℑ ?ℒ ?ℓ ?℔ ?ℕ ?№ ?℗ ?℘ ?ℙ ?ℚ ?ℛ ?ℜ ?ℝ ?℞ ?℟ ?℠ ?℡ + ?™ ?℣ ?ℤ ?℥ ?Ω ?℧ ?ℨ ?℩ ?K ?Å ?ℬ ?ℭ ?℮ ?ℯ ?ℰ ?ℱ ?Ⅎ + ?ℳ ?ℴ ?ℵ ?ℶ ?ℷ ?ℸ ?ℹ ?℺ ?℻ ?ℼ ?ℽ ?ℾ ?ℿ ?⅀ ?⅁ ?⅂ ?⅃ + ?⅄ ?ⅅ ?ⅆ ?ⅇ ?ⅈ ?ⅉ ?⅊ ?⅋ ?⅌ ?⅍ ?ⅎ ?⅏)) (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