michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/src/emacs/lean-variable.el

46 lines
1.4 KiB
EmacsLisp
Raw Normal View History

feat(emacs): implement lean-show-type
2014-08-14 00:02:49 +00:00
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
refactor(emacs/lean-server): use global-server-message-to-process We are using asynchronous process mechanism to communicate between lean-server and emacs. A sender function like lean-eldoc-documentation-function sends a command and waits until lean-global-server-message-to-process is non-nil. When a message is received from lean-server, a filter function lean-server-output-filter is triggered. This filter function concatenates a received message to the buffer until it sees the end of message markers (-- END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer messages into pre, body, and post parts. Then it assembles a message to process and attaches the message to lean-global-server-message-to-process variable. A sender function which is watching for the variable will recognize it, exit the polling, and process the message.
2014-08-25 18:40:37 +00:00
(defvar lean-global-info-record nil
"A placeholder we save the info-record that we get from lean server")
feat(emacs): implement lean-show-type
2014-08-14 00:02:49 +00:00
refactor(emacs/lean-server): use global-server-message-to-process We are using asynchronous process mechanism to communicate between lean-server and emacs. A sender function like lean-eldoc-documentation-function sends a command and waits until lean-global-server-message-to-process is non-nil. When a message is received from lean-server, a filter function lean-server-output-filter is triggered. This filter function concatenates a received message to the buffer until it sees the end of message markers (-- END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer messages into pre, body, and post parts. Then it assembles a message to process and attaches the message to lean-global-server-message-to-process variable. A sender function which is watching for the variable will recognize it, exit the polling, and process the message.
2014-08-25 18:40:37 +00:00
(defvar lean-global-server-message-to-process nil
"A shared variable contains a received message to process.
feat(emacs): implement lean-show-type
2014-08-14 00:02:49 +00:00
refactor(emacs/lean-server): use global-server-message-to-process We are using asynchronous process mechanism to communicate between lean-server and emacs. A sender function like lean-eldoc-documentation-function sends a command and waits until lean-global-server-message-to-process is non-nil. When a message is received from lean-server, a filter function lean-server-output-filter is triggered. This filter function concatenates a received message to the buffer until it sees the end of message markers (-- END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer messages into pre, body, and post parts. Then it assembles a message to process and attaches the message to lean-global-server-message-to-process variable. A sender function which is watching for the variable will recognize it, exit the polling, and process the message.
2014-08-25 18:40:37 +00:00
A message is in the form of (TYPE PRE BODY)
where TYPE := INFO | SET | EVAL | ERROR,
PRE is a server message comes before the message
BODY is a body of the received message.")
(defvar lean-global-server-process nil
"lean server process")
refactor(lean-variable): init server-buffer and current-file-name with nil
2014-08-25 23:25:53 +00:00
(defvar lean-global-server-buffer nil
refactor(emacs/lean-server): use global-server-message-to-process We are using asynchronous process mechanism to communicate between lean-server and emacs. A sender function like lean-eldoc-documentation-function sends a command and waits until lean-global-server-message-to-process is non-nil. When a message is received from lean-server, a filter function lean-server-output-filter is triggered. This filter function concatenates a received message to the buffer until it sees the end of message markers (-- END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer messages into pre, body, and post parts. Then it assembles a message to process and attaches the message to lean-global-server-message-to-process variable. A sender function which is watching for the variable will recognize it, exit the polling, and process the message.
2014-08-25 18:40:37 +00:00
"Global buffer used to store messages sent by lean server")
feat(emacs): implement lean-show-type
2014-08-14 00:02:49 +00:00
refactor(lean-variable): init server-buffer and current-file-name with nil
2014-08-25 23:25:53 +00:00
(defvar lean-global-server-current-file-name nil
feat(emacs): implement lean-show-type
2014-08-14 00:02:49 +00:00
"Current filename that lean server is processing")
(defvar-local lean-changed-lines nil
"Changed lines")
(defvar-local lean-removed-lines nil
"Removed lines")
(defvar-local lean-inserted-lines nil
"Inserted lines")
(defvar lean-global-before-change-beg nil
"Before-change BEG")
(defvar lean-global-before-change-end nil
"Before-change END")
(defvar lean-global-before-change-beg-line-number nil
"Before-change BEG line-number")
(defvar lean-global-before-change-end-line-number nil
"Before-change END line-number")
(defvar lean-global-before-change-text ""
"Before-change text")
(provide 'lean-variable)
Reference in a new issue Copy permalink