feat(emacs): add lean-complete-tag (tab)

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                 |

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")

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)