From 72e1dfa296f3c1285b9be7ccd9cbae0fbb00aa0c Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 3 Sep 2014 00:39:54 -0700 Subject: [PATCH] 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 | 37 ++------------- src/emacs/lean-server.el | 96 ++++++++++++++++++++++++++++---------- src/emacs/lean-settings.el | 3 ++ src/emacs/lean-tags.el | 6 +-- src/emacs/lean-type.el | 62 +++++++++--------------- src/emacs/lean-variable.el | 4 +- 6 files changed, 107 insertions(+), 101 deletions(-) diff --git a/src/emacs/lean-option.el b/src/emacs/lean-option.el index 3c14cc3f5e..7f9c044f58 100644 --- a/src/emacs/lean-option.el +++ b/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)) - (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))))) + (lean-server-send-cmd (lean-cmd-set option-name option-value) 'message))) (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)) - (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 - (`(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))) - (`(,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) + (lean-server-send-cmd (lean-cmd-options) + '(lambda (option-record-alist) + (setq lean-global-option-record-alist + option-record-alist))))) (provide 'lean-option) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index abed40316d..939d2ac4f2 100644 --- a/src/emacs/lean-server.el +++ b/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) - (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)))) + (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))))) (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)) - (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))))) + (setq lean-global-server-buffer (concat lean-global-server-buffer str))) (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) - (cancel-timer lean-global-nay-retry-timer)) - (setq lean-global-nay-retry-timer nil)) + (when (timerp lean-global-retry-timer) + (cancel-timer lean-global-retry-timer)) + (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" - "================" "\n" - "%s\n" - "================" "\n") - string-to-send) + (string-join + '("Send" + "================" + "%s" + "================") "\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) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index c947d9f1e5..210be35757 100644 --- a/src/emacs/lean-settings.el +++ b/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 diff --git a/src/emacs/lean-tags.el b/src/emacs/lean-tags.el index c695f133ab..b1b1d9a191 100644 --- a/src/emacs/lean-tags.el +++ b/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))) - (when full-name - (find-tag full-name)))) + (lean-get-full-name-at-point + (lambda (full-name) + (when full-name (find-tag full-name))))) (defun lean-complete-tag () "complete with tag" diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index bd4e4a872d..a590c43625 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -14,41 +14,35 @@ (require 'lean-debug) (require 'flymake) -(defun lean-fill-placeholder () - "Fill the placeholder with a synthesized expression by Lean." - (interactive) - (let* ((info-record (lean-get-info-record-at-point)) - (synth (and info-record (cl-first (lean-info-record-synth info-record))))) +(setq-local lexical-binding t) + +(defun lean-fill-placeholder-cont (info-record) + "Continuation for lean-fill-placeholder" + (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 ")"))) - (delete-forward-char 1) - (insert synth-str))))) + (when (char-equal (char-after (point)) ?_) + (delete-forward-char 1) + (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) - (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)))))) + (lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont)) ;; ======================================================= ;; 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)) - (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 - (`(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)))) + (lean-server-send-cmd (lean-cmd-eval lean-cmd) + 'message)) ;; Clear Cache (defun lean-clear-cache () diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index a4414e9dad..e9f0d3f5ce 100644 --- a/src/emacs/lean-variable.el +++ b/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 - "Timer used to re-try eldoc-documentation-function for NAY.") +(defvar lean-global-retry-timer nil + "Timer used to re-try event-handler-function.") (defvar-local lean-changed-lines nil "Changed lines")