From 224a4feba295ff0b4d6e2ca8f9edf3f60a830fb1 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 26 Aug 2014 23:58:02 -0700
Subject: [PATCH] fix(emacs/lean-type): problem with lean-eldoc-nay-retry-time

If (current-idle-time) is non-zero, we need to set a timer to run
eldoc-documentation-function again when idle-time = (current-idle-time)
+ retry-delay.
---
 src/emacs/lean-info.el     | 33 +++++++++++++++++----------------
 src/emacs/lean-settings.el |  2 +-
 src/emacs/lean-type.el     | 10 ++++++----
 3 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el
index 32c3f150f4..53bf38b3ba 100644
--- a/src/emacs/lean-info.el
+++ b/src/emacs/lean-info.el
@@ -501,22 +501,23 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
 
 (defun lean-get-info-record (file-name line-number column-number)
   "Get info list from lean server using file-name and line-number"
-  (lean-server-check-current-file file-name)
-  (lean-server-send-cmd (lean-cmd-info line-number))
-  (while (not lean-global-server-message-to-process)
-    (accept-process-output (lean-server-get-process) 0 50 t))
-  (pcase lean-global-server-message-to-process
-    (`(INFO ,pre ,body)
-     (lean-server-log "The following pre-message will be thrown away:")
-     (lean-server-log "%s" pre)
-     (setq lean-global-server-message-to-process nil)
-     (lean-info-record-parse body file-name column-number))
-    (`(,type ,pre , body)
-     (lean-server-log "The following pre-message will be thrown away:")
-     (lean-server-log "%s" pre)
-     (lean-server-log "Something other than INFO detected: %S" type)
-     ;; (lean-server-log "Body: %S" body)
-     (setq lean-global-server-message-to-process nil))))
+  (when (and file-name line-number column-number)
+    (lean-server-check-current-file file-name)
+    (lean-server-send-cmd (lean-cmd-info line-number))
+    (while (not lean-global-server-message-to-process)
+      (accept-process-output (lean-server-get-process) 0 50 t))
+    (pcase lean-global-server-message-to-process
+      (`(INFO ,pre ,body)
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (setq lean-global-server-message-to-process nil)
+       (lean-info-record-parse body file-name column-number))
+      (`(,type ,pre , body)
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (lean-server-log "Something other than INFO detected: %S" type)
+       ;; (lean-server-log "Body: %S" body)
+       (setq lean-global-server-message-to-process nil)))))
 
 (defun lean-get-info-record-at-point ()
   "Get info-record at the current point"
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 77f49886c3..866783e608 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -45,7 +45,7 @@
   :group 'lean
   :type 'boolean)
 
-(defcustom lean-eldoc-nay-retry-time 0.1
+(defcustom lean-eldoc-nay-retry-time 0.3
   "When eldoc-function had nay, try again after this amount of time.")
 
 (defcustom lean-flycheck-checker-name "lmake"
diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el
index 3ef82420b5..d6acb727dc 100644
--- a/src/emacs/lean-type.el
+++ b/src/emacs/lean-type.el
@@ -35,10 +35,12 @@
         info-string)
     (cond
      ((and info-record (lean-info-record-nay info-record))
-      (lean-server-log "NAY Detected")
-      (run-with-idle-timer lean-eldoc-nay-retry-time
-                           nil
-                           'lean-eldoc-documentation-function)
+      (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))