fix(emacs/lean-tags): handle exceptions from find-tag

src/emacs/lean-info.el

@@ -655,6 +655,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
 
 (defun lean-get-full-name-at-point-cont (info-record)
   "Continuation of lean-get-full-name-at-point"
+  (lean-server-debug "lean-get-full-name-at-point-cont: %S" info-record)
   (let ((id (cl-first (lean-info-record-identifier info-record))))
     (when id
       (lean-info-identifier-body-str id))))
@@ -663,7 +664,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
   "Return the full-name at point (if any)"
   (lean-get-info-record-at-point
    (lambda (info-record)
-     (lean-server-debug "executing continuation for get-full-name-at-point")
+     (lean-server-debug "lean-get-full-name-at-point: executing continuation for get-full-name-at-point")
      (funcall cont
               (lean-get-full-name-at-point-cont info-record)))))
 

src/emacs/lean-mode.el

@@ -158,8 +158,7 @@ enabled and disabled respectively.")
   (when lean-eldoc-use
     (set (make-local-variable 'eldoc-documentation-function)
          'lean-eldoc-documentation-function)
-    (eldoc-mode t)
-    (lean-eldoc-documentation-function))
+    (eldoc-mode t))
   ;; company-mode
   (when lean-company-use
     (company-lean-hook)))

src/emacs/lean-server.el

@@ -39,7 +39,8 @@
   "Display a message at the bottom of the *lean-server* buffer."
   (lean-server-output-to-buffer (lean-server-get-buffer)
                               (concat format-string)
-                              args))
+                              args)
+  (apply 'lean-server-debug (cons format-string args)))
 
 (defun lean-server-trace (format-string &rest args)
   "Display a message at the bottom of the *lean-server* buffer."
@@ -486,7 +487,9 @@ Otherwise, set an idle-timer to call the handler again"
          (lean-server-async-task-queue-pop-front)
          (lean-server-debug "event-handler: processed. now the queue size = %d\n"
                             (lean-server-async-task-queue-len))
-         ret)))
+         ret)
+        (t (lean-server-debug "event-handler: not processed. now the queue size = %d\n"
+                              (lean-server-async-task-queue-len)))))
     (if lean-global-async-task-queue (lean-server-set-timer-for-event-handler))))
 
 (defun lean-server-after-save ()

src/emacs/lean-tags.el

@@ -48,7 +48,11 @@
   (interactive)
   (lean-get-full-name-at-point
    (lambda (full-name)
-     (when full-name (find-tag full-name)))))
+     (lean-server-debug "lean-find-tag: %s" full-name)
+     (when full-name
+       (condition-case err
+           (find-tag full-name)
+         (user-error (message "lean-find-tag error: %s" (cdr err))))))))
 
 (defun lean-complete-tag ()
   "complete with tag"