From 030eec1d064b317d7a70ed32d20e9ef8311efdc2 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Fri, 15 Aug 2014 21:23:36 -0700
Subject: [PATCH] feat(emacs): add lean-complete-tag (tab)

---
 src/emacs/README.md    |  1 +
 src/emacs/lean-mode.el |  3 ++-
 src/emacs/lean-tags.el | 18 +++++++++++++-----
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/emacs/README.md b/src/emacs/README.md
index a7cd09b233..8973238ce6 100644
--- a/src/emacs/README.md
+++ b/src/emacs/README.md
@@ -62,3 +62,4 @@ Key Bindings
 |<kbd>C-c C-t</kbd> | lean-eldoc-documentation-function |
 |<kbd>C-c C-f</kbd> | lean-fill-placeholder             |
 |<kbd>M-.</kbd>     | lean-find-tag                     |
+|<kbd>TAB</kbd>     | lean-complete-tag                 |
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 5ef4d977b8..d59270afbf 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -50,7 +50,8 @@
   (local-set-key "\C-c\C-k" 'lean-hott-exe)
   (local-set-key "\C-c\C-t" 'lean-eldoc-documentation-function)
   (local-set-key "\C-c\C-f" 'lean-fill-placeholder)
-  (local-set-key "\M-."     'lean-find-tag))
+  (local-set-key "\M-."     'lean-find-tag)
+  (local-set-key [tab]      'lean-complete-tag))
 
 (define-abbrev-table 'lean-mode-abbrev-table '(
     ("var"    "variable")
diff --git a/src/emacs/lean-tags.el b/src/emacs/lean-tags.el
index 76e9db22ff..fa974df872 100644
--- a/src/emacs/lean-tags.el
+++ b/src/emacs/lean-tags.el
@@ -4,17 +4,25 @@
 ;; Author: Soonho Kong
 ;;
 
+(defun lean-run-lmake-tag ()
+  (let ((ltags-file-name (lean-get-executable "lmake")))
+    (call-process ltags-file-name nil nil nil "TAGS" "--jobs" "--keep-going" "--permissive")))
+
 (defun lean-find-tag ()
   "lean-find-tag"
   (interactive)
-  (let ((ltags-file-name (lean-get-executable "lmake"))
-        (bounds (bounds-of-thing-at-point 'symbol))
+  (let ((bounds (bounds-of-thing-at-point 'symbol))
         symbol-name)
     (when bounds
       (setq symbol-name (buffer-substring-no-properties (car bounds) (cdr bounds)))
-      ;; run ltags
-      (message ltags-file-name)
-      (call-process ltags-file-name nil nil nil "TAGS" "--jobs" "--keep-going" "--permissive")
+      (lean-run-lmake-tag)
       (find-tag symbol-name))))
+
+(defun lean-complete-tag ()
+  "complete with tag"
+  (interactive)
+  (lean-run-lmake-tag)
+  (complete-tag))
 (setq tags-revert-without-query t)
+
 (provide 'lean-tags)