michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-mode): run company-lean--check-prefix before auto-complete

Browse source 
fix #191
This commit is contained in:
Soonho Kong 2014-09-14 23:07:17 -07:00
parent 27b20c5585
commit 1527efb108
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/emacs/lean-company.el
View file

@ -22,6 +22,12 @@
(setq-local company-begin-commands '(self-insert-command)) ; start autocompletion only after typing (setq-local company-begin-commands '(self-insert-command)) ; start autocompletion only after typing
(company-mode t)) (company-mode t))
(defun company-lean--check-prefix ()
"Check whether to use company-lean or not"
(or (company-lean--import-prefix)
(company-lean--findg-prefix)
(company-lean--findp-prefix)))
(defun company-lean--import-remove-lean (file-name) (defun company-lean--import-remove-lean (file-name)
(cond (cond
((s-ends-with? "/default.lean" file-name) ((s-ends-with? "/default.lean" file-name)

6
src/emacs/lean-mode.el
View file

@ -67,9 +67,9 @@
(interactive) (interactive)
(if (minibufferp) (if (minibufferp)
(minibuffer-complete) (minibuffer-complete)
(cond (lean-company-use (cond ((and lean-company-use (company-lean--check-prefix))
(or (company-complete) (company-complete-common))
(eri-indent))) (lean-company-use (eri-indent))
((lean-check-expansion) ((lean-check-expansion)
(completion-at-point-functions)) (completion-at-point-functions))
(t (eri-indent))))) (t (eri-indent)))))