fix(emacs/lean-mode.el): invoke lean from project root if existent

This commit is contained in:
Sebastian Ullrich 2016-04-06 20:48:52 +02:00 committed by Leonardo de Moura
parent 543d7702f0
commit 08c55754a9
3 changed files with 5 additions and 3 deletions

View file

@ -84,8 +84,6 @@
(defun company-lean--import-candidates (prefix)
(let* ((cur-dir (f-dirname (buffer-file-name)))
(parent-dir (f-parent cur-dir))
(project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it))
(f-dirname (buffer-file-name))))
(candidates
(cond
;; prefix = ".."

View file

@ -150,6 +150,7 @@ will be flushed everytime it's executed."
(pcase (lean-choose-minor-mode-based-on-extension)
(`standard "--lean")
(`hott "--hlean")))
(default-directory (or (lean-project-find-root) default-directory))
(process-args (append `(,process-name
,process-buffer-name
,(lean-get-executable lean-executable-name)

View file

@ -11,7 +11,10 @@
"Project file name")
(defun lean-project-find-root ()
(lean-find-file-upward lean-project-file-name))
(let ((p (f--traverse-upwards (f-exists? (f-expand lean-project-file-name it))
(f-dirname (buffer-file-name)))))
(if p (file-name-as-directory p)
nil)))
(defun lean-project-inside-p ()
(if (lean-project-find-root) t nil))