diff --git a/src/emacs/lean-tags.el b/src/emacs/lean-tags.el
index 1fe4290cf..3d8fa45ee 100644
--- a/src/emacs/lean-tags.el
+++ b/src/emacs/lean-tags.el
@@ -7,20 +7,24 @@
 (require 'dash)
 
 (defun lean-generate-tags ()
-  "Run lmake TAGS."
+  "Run lmake TAGS and let emacs use the generated TAGS file."
   (interactive)
-  (let ((ltags-file-name (lean-get-executable "lmake")))
-    (call-process ltags-file-name nil nil nil "TAGS" "--jobs" "--keep-going" "--permissive")))
+  (let ((ltags-file-name (lean-get-executable "lmake"))
+        tags-file-name)
+    (call-process ltags-file-name nil nil nil "TAGS" "--jobs" "--keep-going" "--permissive"))
+  (unless tags-table-list
+    (setq tags-file-name (lean-find-file-upward "TAGS"))
+    (when tags-file-name
+      (visit-tags-table tags-file-name))))
 
 (defmacro lean-tags-make-advice-to-call-ltags (f)
   (let* ((f-name (symbol-name f))
          (advice-name (concat "lean-tags-advice-"
-                             (symbol-name f))))
+                              (symbol-name f))))
     `(defadvice ,f
        (before ,(intern advice-name)  first activate)
        ,(concat "Before call " f-name ", run 'lmake TAGS'")
        (when (derived-mode-p 'lean-mode)
-         (message ,(concat advice-name " is running"))
          (lean-generate-tags)))))
 
 (defvar-local functions-to-call-ltags-before-it
diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index 931020e32..400395339 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -11,6 +11,15 @@
   (cl-reduce (lambda (p1 p2) (concat (file-name-as-directory p1) p2))
              seq))
 
+(defun lean-find-file-upward (file-name &optional dir-name)
+  "Try to find a file in a (current) directory or its parent directories."
+  (let* ((dir-name (or dir-name (file-name-directory (buffer-file-name))))
+         (parent-dir-name (file-name-directory (directory-file-name dir-name)))
+         (full-name (lean-concat-paths dir-name file-name)))
+    (cond ((file-exists-p full-name) full-name)
+          ((string= dir-name parent-dir-name) nil)
+          (t (lean-find-file-upward file-name parent-dir-name)))))
+
 (defun lean-grab-line (n)
   "Return the contents of n-th line at the current buffer"
   (let* ((cur-line-number (line-number-at-pos))