From 343a9a690e00a4a006d1db3b3969cf537b0273b2 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 14 Oct 2014 09:27:25 -0700
Subject: [PATCH] feat(emacs/lean-type): add lean-show-type-add-to-kill-ring
 option

If a customization option 'lean-show-type-add-to-kill-ring' is non-nil
and a user runs 'lean-show-type' by explicitly typing 'C-c C-t',
lean-mode saves the displayed type information message into kill-ring
, which can be pasted by yank (C-y) command.

Close #245
---
 src/emacs/lean-mode.el     |  2 +-
 src/emacs/lean-settings.el |  7 +++++++
 src/emacs/lean-type.el     | 16 +++++++++++++---
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index f71056a54..fd14cb77e 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -87,7 +87,7 @@
   (local-set-key "\C-c\C-l"  'lean-std-exe)
   (local-set-key "\C-c\C-o"  'lean-set-option)
   (local-set-key "\C-c\C-e"  'lean-eval-cmd)
-  (local-set-key "\C-c\C-t"  'lean-eldoc-documentation-function)
+  (local-set-key "\C-c\C-t"  'lean-show-type)
   (local-set-key "\C-c\C-f"  'lean-fill-placeholder)
   (local-set-key "\M-."      'lean-find-tag)
   (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete))
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 54ea8f3fb..b8864c07f 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -122,4 +122,11 @@ written."
   :type 'sexp
   :risky t)
 
+(defcustom lean-show-type-add-to-kill-ring nil
+  "If it is non-nil, add the type information to the kill-ring so
+that user can yank(paste) it later. By default, it's
+false (nil)."
+  :group 'lean
+  :type 'boolean)
+
 (provide 'lean-settings)
diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el
index cb24a00ea..2ce6f6fb2 100644
--- a/src/emacs/lean-type.el
+++ b/src/emacs/lean-type.el
@@ -33,13 +33,16 @@
   (interactive)
   (lean-get-info-record-at-point 'lean-fill-placeholder-cont))
 
-(defun lean-eldoc-documentation-function-cont (info-record)
+(defun lean-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring)
   "Continuation for lean-eldoc-documentation-function"
   (let ((info-string (lean-info-record-to-string info-record)))
     (when info-string
+      (when add-to-kill-ring
+        (kill-new
+         (substring-no-properties info-string)))
       (message "%s" info-string))))
 
-(defun lean-eldoc-documentation-function ()
+(defun lean-eldoc-documentation-function (&optional add-to-kill-ring)
   "Show information of lean expression at point if any"
   (interactive)
   (cond ((and lean-flycheck-use
@@ -50,7 +53,14 @@
                   (not (eolp)))
              (and (looking-back (rx (not white)))
                   (not (bolp))))
-         (lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont))))
+         (lean-get-info-record-at-point
+          (lambda (info-record)
+            (lean-eldoc-documentation-function-cont info-record add-to-kill-ring))))))
+
+(defun lean-show-type ()
+  "Show information of lean-expression at point if any."
+  (interactive)
+  (lean-eldoc-documentation-function lean-show-type-add-to-kill-ring))
 
 ;; =======================================================
 ;; eval