feat(emacs/lean-type): maintain nay-retry timer

src/emacs/lean-server.el

@@ -88,7 +88,10 @@
   "Initialize lean-server related global variables"
   (setq lean-global-server-buffer nil)
   (setq lean-global-server-current-file-name nil)
-  (setq lean-global-server-message-to-process nil))
+  (setq lean-global-server-message-to-process nil)
+  (when (timerp lean-global-nay-retry-timer)
+    (cancel-timer lean-global-nay-retry-timer))
+  (setq lean-global-nay-retry-timer nil))
 
 (defun lean-server-create-process ()
   "Create lean-server process."

src/emacs/lean-type.el

@@ -31,16 +31,20 @@
 (defun lean-eldoc-documentation-function ()
   "Show information of lean expression at point if any"
   (interactive)
+  (when (timerp lean-global-nay-retry-timer)
+    (cancel-timer lean-global-nay-retry-timer)
+    (setq lean-global-nay-retry-timer nil))
   (let ((info-record (lean-get-info-record-at-point))
         info-string)
     (cond
      ((and info-record (lean-info-record-nay info-record))
-      (run-with-idle-timer
-       (if (current-idle-time)
-           (time-add (seconds-to-time lean-eldoc-nay-retry-time) (current-idle-time))
-         lean-eldoc-nay-retry-time)
-       nil
-       'lean-eldoc-documentation-function)
+      (setq lean-global-nay-retry-timer
+            (run-with-idle-timer
+             (if (current-idle-time)
+                 (time-add (seconds-to-time lean-eldoc-nay-retry-time) (current-idle-time))
+               lean-eldoc-nay-retry-time)
+             nil
+             'lean-eldoc-documentation-function))
       nil)
      (info-record
       (setq info-string (lean-info-record-to-string info-record))

src/emacs/lean-variable.el

@@ -24,6 +24,9 @@ where TYPE := INFO | SET | EVAL | ERROR,
 (defvar lean-global-server-current-file-name nil
   "Current filename that lean server is processing")
 
+(defvar lean-global-nay-retry-timer nil
+  "Timer used to re-try eldoc-documentation-function for NAY.")
+
 (defvar-local lean-changed-lines nil
   "Changed lines")
 (defvar-local lean-removed-lines nil