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

fix(emacs): don't pass --lean option

Browse source
This commit is contained in:
Sebastian Ullrich 2016-09-29 17:40:12 -04:00 • committed by Leonardo de Moura
parent ecb6f56e3f
commit 515da8bbb7
2 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -126,7 +126,7 @@
(defun lean-exec-at-pos (process-name process-buffer-name &rest options)
"Execute Lean by providing current position with optional
agruments. The output goes to 'process-buffer-name' buffer, which
arguments. The output goes to 'process-buffer-name' buffer, which
will be flushed everytime it's executed."
(setq g-lean-exec-at-pos-buf "")
;; Kill process-name if exists
@ -152,12 +152,10 @@ will be flushed everytime it's executed."
(if (s-equals? (buffer-file-name) target-file-name)
`("--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)
,lean-mode-option
"--dir"
,(f-dirname (buffer-file-name))
"--line"

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

@ -46,12 +46,10 @@
(interactive)
(let* ((lean-path-env-list
(parse-colon-path (getenv "LEAN_PATH")))
(lean-mode-option "--lean")
(lean--path-list
(parse-colon-path
(ignore-errors
(car (process-lines (lean-get-executable lean-executable-name)
lean-mode-option
"--path")))))
(project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it))
(f-dirname (buffer-file-name))))