michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-server): limit the number of NAY retries

Browse source 
Also, only retry when there is no continuation other than the current
one.
This commit is contained in:
Soonho Kong 2014-09-05 23:04:22 -07:00
parent bdb91f6783
commit bd17d07ebc
3 changed files with 46 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/emacs/lean-info.el
View file

@ -556,8 +556,20 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
(lean-server-send-cmd-async (lean-cmd-info line-number)
(lambda (info-record)
(cond ((lean-info-record-nay info-record)
(lean-get-info-record-at-point cont))
(t (funcall cont info-record)))))))
(lean-server-debug "executing continucation for get-info-record-at-point %d: NAY DETECTED"
lean-global-nay-retry-counter)
(setq lean-global-nay-retry-counter (1+ lean-global-nay-retry-counter))
(if (and (< lean-global-nay-retry-counter
lean-global-nay-retry-counter-max)
(= (length lean-global-async-task-queue) 1))
;; Retry
(lean-get-info-record-at-point cont)
;; Stop
(setq lean-global-nay-retry-counter 0)))
(t
(lean-server-debug "executing continucation for get-info-record-at-point: OK")
(setq lean-global-nay-retry-counter 0)
(funcall cont info-record)))))))
(defun lean-get-full-name-at-point-cont (info-record)
"Continuation of lean-get-full-name-at-point"
@ -570,6 +582,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
(lean-get-info-record-at-point
(lambda (info-record)
(funcall cont
(lean-server-debug "executing continuation for get-full-name-at-point")
(lean-get-full-name-at-point-cont info-record)))))
(provide 'lean-info)

32
src/emacs/lean-server.el
View file

@ -159,6 +159,7 @@
(setq lean-global-server-message-to-process nil)
(setq lean-global-server-last-time-sent nil)
(setq lean-global-async-task-queue nil)
(setq lean-global-nay-retry-counter 0)
(lean-server-cancel-retry-timer))
(defun lean-server-create-process ()
@ -323,26 +324,41 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
(setq result (lean-server-process-message-with-cont body type cont))
`(PROCESSED ,result)))))
(defun lean-server-async-task-queue-len ()
(length lean-global-async-task-queue))
(defun lean-server-async-task-queue-push-back (cont)
(setq lean-global-async-task-queue (-snoc lean-global-async-task-queue cont)))
(defun lean-server-async-task-queue-peek-front ()
(car lean-global-async-task-queue))
(defun lean-server-async-task-queue-pop-front ()
(!cdr lean-global-async-task-queue))
(defun lean-server-send-cmd-async (cmd &optional cont)
"Send cmd to lean-server and attach continuation to the queue."
(lean-server-debug "send-cmd-async: %S %S" (lean-cmd-type cmd) (cl-second cmd))
(lean-server-debug "send-cmd-async: queue len = %d" (length lean-global-async-task-queue))
(lean-server-debug "send-cmd-async: queue len = %d" (lean-server-async-task-queue-len))
(lean-server-send-cmd cmd)
(when cont
(setq lean-global-async-task-queue (-snoc lean-global-async-task-queue cont))
(lean-server-async-task-queue-push-back cont)
(lean-server-debug "send-cmd-async: added to the queue = %S"
(length lean-global-async-task-queue))
(lean-server-async-task-queue-len))
(lean-server-debug "send-cmd-async: call handler")
(lean-server-set-timer-for-event-handler)))
(defun lean-server-consume-all-async-tasks ()
(lean-server-debug "lean-server-consume-all-async-tasks")
(while lean-global-async-task-queue
(accept-process-output (lean-server-get-process) 0 50 t)
(let* ((cont (car lean-global-async-task-queue))
(let* ((cont (lean-server-async-task-queue-peek-front))
(result (lean-server-check-and-process-buffer-with-cont cont)))
(pcase result
(`(PROCESSED ,ret)
(!cdr lean-global-async-task-queue))))))
(lean-server-async-task-queue-pop-front)
(lean-server-debug "lean-server-consume-all-sync-tasks: processed. queue size = %d"
(lean-server-async-task-queue-len)))))))
(defun lean-server-send-cmd-sync (cmd &optional cont)
"Send cmd to lean-server (sync)."
@ -416,11 +432,13 @@ If it's successful, take it out from the queue.
Otherwise, set an idle-timer to call the handler again"
(lean-server-cancel-retry-timer)
(when (eq major-mode 'lean-mode)
(let* ((cont (car lean-global-async-task-queue))
(let* ((cont (lean-server-async-task-queue-peek-front))
(result (lean-server-check-and-process-buffer-with-cont cont)))
(pcase result
(`(PROCESSED ,ret)
(!cdr lean-global-async-task-queue)
(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)))
(if lean-global-async-task-queue (lean-server-set-timer-for-event-handler))))

6
src/emacs/lean-variable.el
View file

@ -27,6 +27,12 @@ where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | FINDP | ERROR,
(defvar lean-global-server-last-time-sent nil
"Last time lean-mode sent a command to lean-server")
(defvar lean-global-nay-retry-counter 0
"Counter for the number of retries for NAY INFO.")
(defvar lean-global-nay-retry-counter-max 10
"The maximum number of retries for NAY INFO.")
(defvar lean-global-retry-timer nil
"Timer used to re-try event-handler-function.")