From 382bf860fd3d8ede0b9634421aeeae7025b59ee2 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 13 Feb 2015 12:19:25 -0500 Subject: [PATCH] fix(emacs/lean-company): import auto-completion for .hlean files fix #434 --- src/emacs/lean-company.el | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index a04d2a905..c5bf02b77 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -10,6 +10,7 @@ (require 'dash-functional) (require 'f) (require 's) +(require 'lean-util) (require 'lean-tags) (require 'lean-server) @@ -53,8 +54,11 @@ (defun company-lean--import-candidates-main (root-dir) (when root-dir - (let* ((lean-files (f-files root-dir - (lambda (file) (equal (f-ext file) "lean")) + (let* ((target-ext (pcase (lean-choose-minor-mode-based-on-extension) + (`hott "hlean") + (`standard "lean"))) + (lean-files (f-files root-dir + (lambda (file) (equal (f-ext file) target-ext)) t)) ;; Relative to project root-dir (lean-files-r (--map (f-relative it root-dir) lean-files))