diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 69de37f7f..2aa9a1b72 100644 --- a/src/emacs/lean-server.el +++ b/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." diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index d6acb727d..0d2de0828 100644 --- a/src/emacs/lean-type.el +++ b/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)) diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index 8add1f46b..b2fb58156 100644 --- a/src/emacs/lean-variable.el +++ b/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