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

feat(emacs/lean-mode): add lean-exec-at-pos and lean-define-key-binding

Browse source 
Example Usage: add the following in your emacs configuration

(add-hook 'lean-mode-hook '(lambda ()
    (lean-define-key-binding "\C-c\C-g"
                             '(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))

close #499
This commit is contained in:
Soonho Kong 2015-03-24 14:57:49 -04:00
parent d950338980
commit 69d1cfdd52
1 changed files with 52 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -53,6 +53,55 @@
(or arg "")
target-file-name))))
(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
will be flushed everytime it's executed."
;; Kill process-name if exists
(let ((current-process (get-process process-name)))
(when current-process
(kill-process)))
;; Flush process-buffer
(let ((process-buffer (get-buffer process-buffer-name)))
(when process-buffer
(with-current-buffer process-buffer
(erase-buffer))))
;; Ask to save current buffer
(when (buffer-file-name)
(save-some-buffers nil `(lambda () (s-equals? (buffer-file-name) ,(buffer-file-name)))))
;; Start process
(let* ((target-file-name
(or
;; Only use file-name if the current buffer is not modified
(and (not (buffer-modified-p)) (buffer-file-name))
(flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir)))
(cache-file-name
(s-concat (f-no-ext target-file-name)
".clean"))
(cache-option
;; Cache is only used when we use a non-temporary file
(if (s-equals? (buffer-file-name) target-file-name)
`("--cache" ,cache-file-name)
'()))
(lean-mode-option
(pcase (lean-choose-minor-mode-based-on-extension)
(`standard "--lean")
(`hott "--hlean")))
(process-args (append `(,process-name
,process-buffer-name
,(lean-get-executable lean-executable-name)
,lean-mode-option
"--line"
,(int-to-string (line-number-at-pos))
"--col"
,(int-to-string (current-column)))
options
cache-option
`(,target-file-name)))
(p (apply 'start-process process-args)))
(set-process-coding-system p 'utf-8 'utf-8)
(set-process-query-on-exit-flag p nil)))
(defun lean-std-exe ()
(interactive)
(lean-execute))
@ -95,6 +144,9 @@
(local-set-key "\M-." 'lean-find-tag)
(local-set-key (kbd "TAB") 'lean-tab-indent-or-complete))
(defun lean-define-key-binding (key cmd)
(local-set-key key `(lambda () (interactive) ,cmd)))
(define-abbrev-table 'lean-abbrev-table
'())