diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index 7a22a3182..43777ef1a 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -170,10 +170,32 @@ nil) (t t))) +(defun lean-find-id-beg () + (save-excursion + (let ((initial-pos (point)) + (mode 'backward) + stop char-at-pos success) + (while (not stop) + (setq char-at-pos (char-after)) + (cl-case mode + ('backward + (cond + ((lean-id-rest-p char-at-pos) (backward-char 1)) + (t (forward-char 1) + (setq mode 'forward)))) + ('forward + (cond + ((lean-id-first-p char-at-pos) (setq stop t) + (setq success t)) + ((< (point) initial-pos) (forward-char 1)) + (t (setq stop t)))))) + (when success + (point))))) + (defun company-lean--findp-prefix () "Returns the symbol to complete. Also, if point is on a dot, triggers a completion immediately." - (let ((prefix (company-grab-symbol))) + (let ((prefix (lean-grab-id))) (when (and prefix (company-lean--need-autocomplete) diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el index e48b89d70..5f84b07b8 100644 --- a/src/emacs/lean-util.el +++ b/src/emacs/lean-util.el @@ -67,4 +67,58 @@ (-uniq (-map (-compose 'f-slash 'f-canonical) path-list)))) +(defun lean-letter-like-unicode-p (u) + (when u + (cond ((and (<= #x3b1 u) (<= u #x3c9) (not (= u #x3bb))) t) + ((and (<= #x3ca u) (<= u #x3fb)) t) + ((and (<= #x1f00 u) (<= u #x1ffe)) t) + ((and (<= #x2100 u) (<= u #x214f)) t)))) + +(defun lean-super-sub-script-alnum-unicode-p (u) + (when u + (cond ((and (<= #x2070 u) (<= u #x2078)) t) + ((and (<= #x207f u) (<= u #x2089)) t) + ((and (<= #x2090 u) (<= u #x209c)) t)))) + +(defun lean-isalpha (c) + (when c + (cond ((and (<= ?a c) (<= c ?z)) t) + ((and (<= ?A c) (<= c ?Z)) t)))) + +(defun lean-isnum (c) + (when c + (if (and (<= ?0 c) (<= c ?9)) t))) + +(defun lean-isalnum (c) + (when c + (or (lean-isalpha c) + (lean-isnum c)))) + +(defun lean-id-rest-p (c) + (when c + (or (lean-isalnum c) + (= c ?_) + (= c ?\') + (lean-letter-like-unicode-p c) + (lean-super-sub-script-alnum-unicode-p c)))) + +(defun lean-id-first-p (c) + (when c + (or (lean-isalnum c) + (= c ?_) + (lean-letter-like-unicode-p c)))) + +(defun lean-grab-id () + (interactive) + (save-excursion + (when (and (or (eolp) + (looking-at (rx white)) + (eobp)) + (not (bolp))) + (backward-char 1)) + (let ((cur-pos (point)) + (id-beg (lean-find-id-beg))) + (when id-beg + (buffer-substring id-beg (1+ (point))))))) + (provide 'lean-util) diff --git a/src/emacs/test/lean-util-test.el b/src/emacs/test/lean-util-test.el new file mode 100644 index 000000000..9578156a8 --- /dev/null +++ b/src/emacs/test/lean-util-test.el @@ -0,0 +1,83 @@ +;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. +;; Released under Apache 2.0 license as described in the file LICENSE. +;; +;; Author: Soonho Kong +;; + +(require 'ert) +(require 'dash) +(require 'lean-util) + +(ert-deftest lean-test-unicode () + (--map (should (lean-letter-like-unicode-p it)) + (list ?α ?β ?μ ?δ ?ε ?ζ ?η ?θ ?ι ?κ ?μ ?ν ?ξ ?ο + ?π ?ρ ?ς ?σ ?τ ?υ ?υ ?φ ?χ ?ψ ?ω)) + (should (not (lean-letter-like-unicode-p ?λ))) + (should (lean-super-sub-script-alnum-unicode-p ?⁰))) + +(ert-deftest lean-test-isalpha () + (--map (should (lean-isalpha it)) + (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))) + +(ert-deftest lean-test-isnum () + (--map (should (lean-isnum it)) + (list ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9))) + +(ert-deftest lean-test-isalnum () + (--map (should (lean-isalnum it)) + (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 + ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9))) + +(ert-deftest lean-test-letter-like-unicode-p () + (--map (should (lean-letter-like-unicode-p it)) + (list ?α ?β ?γ ?δ ?ε ?ζ ?η ?θ ?ι ?κ ;;?λ + ?μ ?ν ?ξ ?ο ?π ?ρ ?ς ?σ ?τ ?υ + ?φ ?χ ?ψ ?ω)) + (should (not (lean-letter-like-unicode-p ?λ))) + (--map (should (lean-letter-like-unicode-p it)) + (list ?ϊ ?ϋ ?ό ?ύ ?ώ ?Ϗ ?ϐ ?ϑ ?ϒ ?ϓ ?ϔ ?ϕ ?ϖ + ?ϗ ?Ϙ ?ϙ ?Ϛ ?ϛ ?Ϝ ?ϝ ?Ϟ ?ϟ ?Ϡ ?ϡ ?Ϣ ?ϣ + ?Ϥ ?ϥ ?Ϧ ?ϧ ?Ϩ ?ϩ ?Ϫ ?ϫ ?Ϭ ?ϭ ?Ϯ ?ϯ ?ϰ + ?ϱ ?ϲ ?ϳ ?ϴ ?ϵ ?϶ ?Ϸ ?ϸ ?Ϲ ?Ϻ ?ϻ)) + (--map (should (lean-letter-like-unicode-p it)) + (list ?ἀ ?ἁ ?ἂ ?ἃ ?ἄ ?ἅ ?ἆ ?ἇ ?Ἀ ?Ἁ ?Ἂ ?Ἃ ?Ἄ + ?Ἅ ?Ἆ ?Ἇ ?ἐ ?ἑ ?ἒ ?ἓ ?ἔ ?ἕ ?἖ ?἗ ?Ἐ ?Ἑ + ?Ἒ ?Ἓ ?Ἔ ?Ἕ ?἞ ?἟ ?ἠ ?ἡ ?ἢ ?ἣ ?ἤ ?ἥ + ?ἦ ?ἧ ?Ἠ ?Ἡ ?Ἢ ?Ἣ ?Ἤ ?Ἥ ?Ἦ ?Ἧ ?ἰ ?ἱ + ?ἲ ?ἳ ?ἴ ?ἵ ?ἶ ?ἷ ?Ἰ ?Ἱ ?Ἲ ?Ἳ ?Ἴ ?Ἵ ?Ἶ ?Ἷ + ?ὀ ?ὁ ?ὂ ?ὃ ?ὄ ?ὅ ?὆ ?὇ ?Ὀ ?Ὁ ?Ὂ ?Ὃ + ?Ὄ ?Ὅ ?὎ ?὏ ?ὐ ?ὑ ?ὒ ?ὓ ?ὔ ?ὕ ?ὖ ?ὗ + ?὘ ?Ὑ ?὚ ?Ὓ ?὜ ?Ὕ ?὞ ?Ὗ ?ὠ ?ὡ ?ὢ + ?ὣ ?ὤ ?ὥ ?ὦ ?ὧ ?Ὠ ?Ὡ ?Ὢ ?Ὣ ?Ὤ ?Ὥ ?Ὦ + ?Ὧ ?ὰ ?ά ?ὲ ?έ ?ὴ ?ή ?ὶ ?ί ?ὸ ?ό ?ὺ ?ύ ?ὼ + ?ώ ?὾ ?὿ ?ᾀ ?ᾁ ?ᾂ ?ᾃ ?ᾄ ?ᾅ ?ᾆ ?ᾇ ?ᾈ + ?ᾉ ?ᾊ ?ᾋ ?ᾌ ?ᾍ ?ᾎ ?ᾏ ?ᾐ ?ᾑ ?ᾒ ?ᾓ ?ᾔ + ?ᾕ ?ᾖ ?ᾗ ?ᾘ ?ᾙ ?ᾚ ?ᾛ ?ᾜ ?ᾝ ?ᾞ ?ᾟ ?ᾠ ?ᾡ ?ᾢ + ?ᾣ ?ᾤ ?ᾥ ?ᾦ ?ᾧ ?ᾨ ?ᾩ ?ᾪ ?ᾫ ?ᾬ ?ᾭ ?ᾮ ?ᾯ ?ᾰ + ?ᾱ ?ᾲ ?ᾳ ?ᾴ ?᾵ ?ᾶ ?ᾷ ?Ᾰ ?Ᾱ ?Ὰ ?Ά ?ᾼ ?᾽ + ?ι ?᾿ ?῀ ?῁ ?ῂ ?ῃ ?ῄ ?῅ ?ῆ ?ῇ ?Ὲ ?Έ ?Ὴ + ?Ή ?ῌ ?῍ ?῎ ?῏ ?ῐ ?ῑ ?ῒ ?ΐ ?῔ ?῕ ?ῖ ?ῗ + ?Ῐ ?Ῑ ?Ὶ ?Ί ?῜ ?῝ ?῞ ?῟ ?ῠ ?ῡ ?ῢ ?ΰ ?ῤ ?ῥ + ?ῦ ?ῧ ?Ῠ ?Ῡ ?Ὺ ?Ύ ?Ῥ ?῭ ?΅ ?` ?῰ ?῱ ?ῲ ?ῳ + ?ῴ ?῵ ?ῶ ?ῷ ?Ὸ ?Ό ?Ὼ ?Ώ ?ῼ ?´ ?῾)) + (--map (should (lean-letter-like-unicode-p it)) + (list ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ + ?ℏ ?ℐ ?ℑ ?ℒ ?ℓ ?℔ ?ℕ ?№ ?℗ ?℘ ?ℙ ?ℚ ?ℛ ?ℜ ?ℝ + ?℞ ?℟ ?℠ ?℡ ?™ ?℣ ?ℤ ?℥ ?Ω ?℧ ?ℨ ?℩ ?K ?Å ?ℬ + ?ℭ ?℮ ?ℯ ?ℰ ?ℱ ?Ⅎ ?ℳ ?ℴ ?ℵ ?ℶ ?ℷ ?ℸ ?ℹ ?℺ ?℻ + ?ℼ ?ℽ ?ℾ ?ℿ ?⅀ ?⅁ ?⅂ ?⅃ ?⅄ ?ⅅ ?ⅆ ?ⅇ ?ⅈ ?ⅉ ?⅊ + ?⅋ ?⅌ ?⅍ ?ⅎ ?⅏))) + +(ert-deftest lean-test-super-sub-script-alnum-unicode-p () + (--map (should (lean-super-sub-script-alnum-unicode-p it)) + (list ?ₐ ?ₑ ?ₒ ?ₓ ?ₔ ?ₕ ?ₖ ?ₗ ?ₘ ?ₙ ?ₚ ?ₛ ?ₜ)) + (--map (should (lean-super-sub-script-alnum-unicode-p it)) + (list ?ⁿ ?₀ ?₁ ?₂ ?₃ ?₄ ?₅ ?₆ ?₇ ?₈ ?₉)) + (--map (should (lean-super-sub-script-alnum-unicode-p it)) + (list ?⁰ ?ⁱ ?⁲ ?⁳ ?⁴ ?⁵ ?⁶ ?⁷ ?⁸)))