From 69d1cfdd528693b9b2f6e7b53aad63fc3f307b2c Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Mar 2015 14:57:49 -0400
Subject: [PATCH] feat(emacs/lean-mode): add lean-exec-at-pos and
 lean-define-key-binding

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
---
 src/emacs/lean-mode.el | 52 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index c2199892a..5907e2d9e 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -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
   '())