feat(emacs): add lean-find-tag (M-.)

src/emacs/README.md

@@ -61,3 +61,4 @@ Key Bindings
 |<kbd>C-c C-k</kbd> | lean-hott-exe                     |
 |<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                     |

src/emacs/lean-mode.el

@@ -14,6 +14,7 @@
 (require 'lean-flycheck)
 (require 'lean-input)
 (require 'lean-type)
+(require 'lean-tags)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"
@@ -48,14 +49,14 @@
   (local-set-key "\C-c\C-l" 'lean-std-exe)
   (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 "\C-c\C-f" 'lean-fill-placeholder)
+  (local-set-key "\M-."     'lean-find-tag))
 
 (define-abbrev-table 'lean-mode-abbrev-table '(
     ("var"    "variable")
     ("vars"   "variables")
     ("def"    "definition")
-    ("th"     "theorem")
-    ))
+    ("th"     "theorem")))
 
 (define-generic-mode
     'lean-mode     ;; name of the mode to create

src/emacs/lean-tags.el

@@ -0,0 +1,20 @@
+;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Soonho Kong
+;;
+
+(defun lean-find-tag ()
+  "lean-find-tag"
+  (interactive)
+  (let ((ltags-file-name (lean-get-executable "lmake"))
+        (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")
+      (find-tag symbol-name))))
+(setq tags-revert-without-query t)
+(provide 'lean-tags)