Don't depend on Dash

[mekeor]

lean4-mode depends on Dash. This is not too bad. But in recent years, the standard library of ELisp has evolved and this dependency doesn't seem necessary now. These are probably most occurences of functions from Dash:

lean4-input.el:324:      (--each
lean4-input.el:325:          (--filter (not (member (car it) exclude-list))
lean4-info.el:80:  (-if-let (window (get-buffer-window buffer))
lean4-info.el:116:          (-let (((&Diagnostic :message :range (&Range :start (&Position :line :character))) e))
lean4-info.el:124:    (-let* ((deactivate-mark) ; keep transient mark
lean4-info.el:127:            (errors (-sort (-on #'< #'lean4-diagnostic-full-end-line) errors))
lean4-info.el:129:             (--split-with (< (lean4-diagnostic-full-end-line it) line) errors))
lean4-info.el:131:             (--split-with (<= (lean4-diagnostic-full-start-line it) line) errors)))
lean4-info.el:261:    (-some-> lean4-info-buffer-debounce-timer cancel-timer)
lean4-info.el:278:     (-lambda ((ignored &as &lean:PlainGoal? :goals))
lean4-info.el:287:     (-lambda ((ignored &as &lean:PlainTermGoal? :goal))
lean4-syntax.el:89:    (--each (list ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k ?l ?m
lean4-syntax.el:94:    (--each (list ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9)
lean4-syntax.el:96:    (--each (list ?α ?β ?γ ?δ ?ε ?ζ ?η ?θ ?ι ?κ ;;?λ
lean4-syntax.el:100:    (--each (list ?ϊ ?ϋ ?ό ?ύ ?ώ ?Ϗ ?ϐ ?ϑ ?ϒ ?ϓ ?ϔ ?ϕ ?ϖ
lean4-syntax.el:105:    (--each (list ?ἀ ?ἁ ?ἂ ?ἃ ?ἄ ?ἅ ?ἆ ?ἇ ?Ἀ ?Ἁ ?Ἂ ?Ἃ ?Ἄ
lean4-syntax.el:126:    (--each (list ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ
lean4-syntax.el:133:    (--each (list ?₁ ?₂ ?₃ ?₄ ?₅ ?₆ ?₇ ?₈ ?₉ ?₀
lean4-syntax.el:139:    (--each (string-to-list "#$%&*+<=>@^|~:")
lean4-syntax.el:219:    `(,(-concat new-entries inherited-entries))))

[mekeor]

lsp-mode is too tightly coupled to Dash. It's not practical to drop the dependency on Dash for those parts of Lean4-Mode that interface lsp-mode. That's why I'm now moving this ticket to milestone 4.