feat(emacs): implement non-blocking communication

The key idea is to pass a continuation function when we call
lean-server-send-cmd function. The passed continuation function is
called by lean-server-event-handler. Until the buffer is ready, the
event handler will be called in interval (lean-server-retry-time, 0.1
sec by default). When we have 'NAY' for INFO command, it will re-send
INFO commands to lean-server until we have one without 'NAY'.

Close #123

src/emacs/lean-option.el

@@ -22,21 +22,7 @@
                            nil t "" nil (car key-list)))
          (option (cdr (assoc option-name lean-global-option-record-alist)))
          (option-value (lean-option-read option)))
-    (lean-server-send-cmd (lean-cmd-set option-name option-value))
+    (lean-server-send-cmd (lean-cmd-set option-name option-value) 'message)))
-    (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
-      (`(SET ,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-server-log "We have the following response from lean-server")
-       (message "%s" (lean-set-parse-string body)))
-      (`(,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 SET detected: %S" type)
-       (setq lean-global-server-message-to-process nil)))))
 
 (defun lean-option-read-bool (prompt)
   (interactive)
@@ -154,22 +140,9 @@
   "Get Lean option."
   (interactive)
   (unless lean-global-option-record-alist
-    (lean-server-send-cmd (lean-cmd-options))
+    (lean-server-send-cmd (lean-cmd-options)
-    (while (not lean-global-server-message-to-process)
+                          '(lambda (option-record-alist)
-      (accept-process-output (lean-server-get-process) 0 50 t))
-    (pcase lean-global-server-message-to-process
-      (`(OPTIONS ,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-server-log "We have the following response from lean-server")
                              (setq lean-global-option-record-alist
-             (lean-options-parse-string body)))
+                                   option-record-alist)))))
-      (`(,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 SET detected: %S" type)
-       (setq lean-global-server-message-to-process nil))))
-  lean-global-option-record-alist)
 
 (provide 'lean-option)

src/emacs/lean-server.el

@@ -68,24 +68,16 @@
 (defun lean-server-check-buffer-and-partition (buf-str)
   "Return the status of buffer."
   (let (result)
+    (when buf-str
       (cl-loop for (type beg-regex end-regex) in lean-server-syntax-pattern
                do (setq partition-result (lean-server-split-buffer buf-str beg-regex end-regex))
                if partition-result
-             return `(,type ,partition-result))))
+               return `(,type ,partition-result)))))
 
 (defun lean-server-process-received-message (buf str)
   "Process received message from lean-server"
   (lean-server-log "Received String: %s" str)
-  ;; Append to buffer
+  (setq lean-global-server-buffer (concat lean-global-server-buffer str)))
-  (setq lean-global-server-buffer (concat lean-global-server-buffer str))
-  (let ((partition-result (lean-server-check-buffer-and-partition lean-global-server-buffer)))
-    (pcase partition-result
-      (`(,type (,pre ,body ,post))
-       (lean-server-log "PRE: %s" pre)
-       (lean-server-log "BODY: %s" body)
-       (lean-server-log "POST: %s" post)
-       (setq lean-global-server-message-to-process `(,type ,pre ,body))
-       (setq lean-global-server-buffer post)))))
 
 (defun lean-server-output-filter (process string)
   "Filter function attached to lean-server process"
@@ -109,9 +101,9 @@
   (setq lean-global-server-message-to-process nil)
   (setq lean-global-server-last-time-sent nil)
   (setq lean-global-option-record-alist nil)
-  (when (timerp lean-global-nay-retry-timer)
+  (when (timerp lean-global-retry-timer)
-    (cancel-timer lean-global-nay-retry-timer))
+    (cancel-timer lean-global-retry-timer))
-  (setq lean-global-nay-retry-timer nil))
+  (setq lean-global-retry-timer nil))
 
 (defun lean-server-create-process ()
   "Create lean-server process."
@@ -219,22 +211,78 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('EVAL    ())
     ('OPTIONS ())))
 
-(defun lean-server-send-cmd (cmd)
+(defun lean-server-send-cmd (cmd &optional cont)
   "Send string to lean-server."
   (let ((proc (lean-server-get-process))
         (string-to-send (concat (lean-cmd-to-string cmd) "\n")))
     (lean-server-before-send-cmd cmd)
     ;; Logging
     (lean-server-log
-     (concat "Send" "\n"
+     (string-join
-             "================" "\n"
+      '("Send"
-             "%s\n"
+        "================"
-             "================" "\n")
+        "%s"
-     string-to-send)
+        "================") "\n") string-to-send)
     ;; Trace
     (lean-server-trace
      (format "%s" string-to-send))
     (process-send-string proc string-to-send)
-    (lean-server-after-send-cmd cmd)))
+    (lean-server-after-send-cmd cmd)
+    (when cont
+      (lean-server-event-handler cont))))
 
+(defun lean-server-set-timer-for-event-handler (cont)
+  (setq lean-global-retry-timer
+        (run-with-idle-timer
+         (if (current-idle-time)
+             (time-add (seconds-to-time lean-server-retry-time) (current-idle-time))
+           lean-server-retry-time)
+         nil
+         'lean-server-event-handler cont)))
+
+(defun lean-server-get-info-record-at-pos (body)
+  (let* ((file-name (buffer-file-name))
+         (column (current-column))
+         (cur-char (char-after (point))))
+    (when (and cur-char
+               (or (char-equal cur-char ?\s)
+                   (char-equal cur-char ?\t)
+                   (char-equal cur-char ?\t)
+                   (char-equal cur-char ?\,)
+                   (char-equal cur-char ?\))
+                   (char-equal cur-char ?\})
+                   (char-equal cur-char ?\]))
+               (> column 1))
+      (setq column (1- column)))
+    (lean-info-record-parse body file-name column)))
+
+(defun lean-server-event-handler (cont)
+  (let ((partition-result (lean-server-check-buffer-and-partition lean-global-server-buffer)))
+    (pcase partition-result
+      (`(,type (,pre ,body ,post))
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (setq lean-global-server-buffer post)
+       (cl-case type
+         (INFO
+          (let ((info-record (lean-server-get-info-record-at-pos body)))
+            (cond
+             ((lean-info-record-nay info-record)
+              (lean-server-send-cmd (lean-cmd-info (line-number-at-pos))
+                                    cont))
+             (t
+              (funcall cont info-record)))))
+         (SET
+          (funcall cont (lean-set-parse-string body)))
+         (EVAL
+          (funcall cont (lean-eval-parse-string body)))
+         (OPTIONS
+          (funcall cont (lean-options-parse-string body)))
+         (SHOW
+          (funcall cont (lean-show-parse-string body)))
+         (ERROR
+          (lean-server-log "Error detected:\n%s" body))))
+      (`()
+       (lean-server-set-timer-for-event-handler cont)
+       nil))))
 (provide 'lean-server)

src/emacs/lean-settings.el

@@ -48,6 +48,9 @@
 (defcustom lean-eldoc-nay-retry-time 0.3
   "When eldoc-function had nay, try again after this amount of time.")
 
+(defcustom lean-server-retry-time 0.1
+  "Retry interval for event-handler")
+
 (defcustom lean-flycheck-checker-name "linja"
   "lean-flychecker checker name"
   :group 'lean

src/emacs/lean-tags.el

@@ -41,9 +41,9 @@
 (defun lean-find-tag ()
   "lean-find-tag"
   (interactive)
-  (let ((full-name (lean-get-full-name-at-point)))
+  (lean-get-full-name-at-point
-    (when full-name
+   (lambda (full-name)
-      (find-tag full-name))))
+     (when full-name (find-tag full-name)))))
 
 (defun lean-complete-tag ()
   "complete with tag"

src/emacs/lean-type.el

@@ -14,41 +14,35 @@
 (require 'lean-debug)
 (require 'flymake)
 
-(defun lean-fill-placeholder ()
+(setq-local lexical-binding t)
-  "Fill the placeholder with a synthesized expression by Lean."
+
-  (interactive)
+(defun lean-fill-placeholder-cont (info-record)
-  (let* ((info-record (lean-get-info-record-at-point))
+  "Continuation for lean-fill-placeholder"
-         (synth (and info-record (cl-first (lean-info-record-synth info-record)))))
+  (let ((synth (and info-record (cl-first (lean-info-record-synth info-record)))))
     (when synth
       (let ((synth-str
              (replace-regexp-in-string "?M_[0-9]+" "_" (lean-info-synth-body-str synth))))
         (when (search " " synth-str)
           (setq synth-str (concat "(" synth-str ")")))
+        (when (char-equal (char-after (point)) ?_)
           (delete-forward-char 1)
-        (insert synth-str)))))
+          (insert synth-str))))))
+
+(defun lean-fill-placeholder ()
+  "Fill the placeholder with a synthesized expression by Lean."
+  (interactive)
+  (lean-get-info-record-at-point 'lean-fill-placeholder-cont))
+
+(defun lean-eldoc-documentation-function-cont (info-record)
+  "Continuation for lean-eldoc-documentation-function"
+  (let ((info-string (lean-info-record-to-string info-record)))
+    (when info-string
+      (message "%s" info-string))))
 
 (defun lean-eldoc-documentation-function ()
   "Show information of lean expression at point if any"
   (interactive)
-  (when (timerp lean-global-nay-retry-timer)
+  (lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont))
-    (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))
-      (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))
-      (when info-string
-        (message "%s" info-string))))))
 
 ;; =======================================================
 ;; eval
@@ -67,20 +61,8 @@
 (defun lean-eval-cmd (lean-cmd)
   "Evaluate lean command."
   (interactive "sLean CMD: ")
-  (lean-server-send-cmd (lean-cmd-eval lean-cmd))
+  (lean-server-send-cmd (lean-cmd-eval lean-cmd)
-  (while (not lean-global-server-message-to-process)
+                        'message))
-    (accept-process-output (lean-server-get-process) 0 50 t))
-  (pcase lean-global-server-message-to-process
-    (`(EVAL ,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)
-     (message "%s" (lean-eval-parse-string body)))
-    (`(,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 EVAL detected: %S" type)
-     (setq lean-global-server-message-to-process nil))))
 
 ;; Clear Cache
 (defun lean-clear-cache ()

src/emacs/lean-variable.el

@@ -30,8 +30,8 @@ where TYPE := INFO | SET | EVAL | OPTIONS | ERROR,
 (defvar lean-global-server-last-time-sent nil
   "Last time lean-mode sent a command to lean-server")
 
-(defvar lean-global-nay-retry-timer nil
+(defvar lean-global-retry-timer nil
-  "Timer used to re-try eldoc-documentation-function for NAY.")
+  "Timer used to re-try event-handler-function.")
 
 (defvar-local lean-changed-lines nil
   "Changed lines")