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
|C-c C-t | lean-eldoc-documentation-function |
|C-c C-f | lean-fill-placeholder |
|M-. | lean-find-tag |
+|TAB | 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)