max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

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

Browse source
This commit is contained in:
Sebastian Ullrich 2016-04-06 20:48:52 +02:00 • committed by Leonardo de Moura
parent 5726d45e7f
commit e3e4f6d648
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -153,6 +153,7 @@ will be flushed everytime it's executed."
`("--cache" ,cache-file-name)
'()))
(lean-mode-option "--lean")
(default-directory (or (lean-project-find-root) default-directory))
(process-args (append `(,process-name
,process-buffer-name
,(lean-get-executable lean-executable-name)

5
src/emacs/lean-project.el
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))