From 1829e64a76dcc627757650119295e4013de18c8a Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 28 Jul 2015 18:10:46 -0700
Subject: [PATCH] feat(emacs/lean-server.el):
 lean-server-consume-all-async-tasks restart lean-server if necessary

related issue: #263
---
 src/emacs/lean-server.el   | 50 +++++++++++++++++++++++---------------
 src/emacs/lean-settings.el |  4 +++
 2 files changed, 35 insertions(+), 19 deletions(-)

diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index 99c94d56f..db51cae02 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -432,25 +432,28 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
                      (lean-server-async-task-queue-len))
   (while lean-global-async-task-queue
     (accept-process-output (lean-server-get-process) 0 50 t)
-    (let* ((front-item (lean-server-async-task-queue-peek-front))
-           (cont       (car front-item))
-           (cmd-type   (cdr front-item))
-           (result (lean-server-check-and-process-buffer-with-cont cont
-                                                                   cmd-type)))
-      (pcase result
-        (`(PROCESSED ,ret)
-         (lean-server-async-task-queue-pop-front)
-                  (lean-debug "lean-server-consume-all-sync-tasks: processed. queue size = %d"
-                            (lean-server-async-task-queue-len)))
-        (`(NOTREADY)
-         (lean-debug "lean-server-consume-all-sync-tasks: not ready. queue size = %d"
-                            (lean-server-async-task-queue-len)))
-        (t
-         (lean-server-async-task-queue-pop-front)
-         (lean-debug "lean-server-consume-all-sync-tasks: either error or quit happend. queue size = %d"
-                            (lean-server-async-task-queue-len))))))
-  (lean-debug "lean-server-consume-all-async-tasks: over. queue size = %d"
-                     (lean-server-async-task-queue-len)))
+    (let ((kill-timer (run-at-time lean-time-to-restart-server nil
+                                   '(lambda () (lean-server-restart-process)))))
+      (let* ((front-item (lean-server-async-task-queue-peek-front))
+             (cont       (car front-item))
+             (cmd-type   (cdr front-item))
+             (result (lean-server-check-and-process-buffer-with-cont cont
+                                                                     cmd-type)))
+        (pcase result
+          (`(PROCESSED ,ret)
+           (lean-server-async-task-queue-pop-front)
+           (lean-debug "lean-server-consume-all-sync-tasks: processed. queue size = %d"
+                       (lean-server-async-task-queue-len)))
+          (`(NOTREADY)
+           (lean-debug "lean-server-consume-all-sync-tasks: not ready. queue size = %d"
+                       (lean-server-async-task-queue-len)))
+          (t
+           (lean-server-async-task-queue-pop-front)
+           (lean-debug "lean-server-consume-all-sync-tasks: either error or quit happend. queue size = %d"
+                       (lean-server-async-task-queue-len)))))
+      (cancel-timer kill-timer)
+      (lean-debug "lean-server-consume-all-async-tasks: over. queue size = %d"
+                  (lean-server-async-task-queue-len)))))
 
 (defun lean-server-send-cmd-sync (cmd &optional cont)
   "Send cmd to lean-server (sync)."
@@ -600,4 +603,13 @@ Otherwise, set an idle-timer to call the handler again"
   (when (buffer-modified-p)
     (lean-server-send-cmd-async (lean-cmd-sync))))
 
+
+;; Sanity Check
+;; ============
+;; Compare the current buffer and the copy that lean-server is
+;; maintaining.
+(defun lean-server-sanity-check-p ()
+  (interactive)
+  (lean-server-send-cmd-async (lean-cmd-show) (lambda (msg) msg)))
+
 (provide 'lean-server)
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 0c6811c44..dec1da7ee 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -151,4 +151,8 @@ false (nil)."
   "Disable this if we don't need to keep track of the changes. A usage
   is to batch-process .org files to .html files")
 
+(defcustom lean-time-to-restart-server 1
+  "After lean-time-to-kill-server passed, we restart lean-server if
+  the all jobs in the queue are not process.")
+
 (provide 'lean-settings)