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

fix(emacs/lean-util): add hlean support in lean-path-list

Browse source 
close #450
This commit is contained in:
Soonho Kong 2015-02-27 15:27:18 -05:00
parent 7d827a14c9
commit c9ffc2fec8
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/emacs/lean-util.el
View file

@ -51,10 +51,15 @@
(interactive) (interactive)
(let* ((lean-path-env-list (let* ((lean-path-env-list
(parse-colon-path (getenv "LEAN_PATH"))) (parse-colon-path (getenv "LEAN_PATH")))
(lean-mode-option
(pcase (lean-choose-minor-mode-based-on-extension)
(`standard "--lean")
(`hott "--hlean")))
(lean--path-list (lean--path-list
(parse-colon-path (parse-colon-path
(ignore-errors (ignore-errors
(car (process-lines (lean-get-executable lean-executable-name) (car (process-lines (lean-get-executable lean-executable-name)
lean-mode-option
"--path"))))) "--path")))))
(project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it)) (project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it))
(f-dirname (buffer-file-name)))) (f-dirname (buffer-file-name))))