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

refactor(emacs/lean-server): lean-server-check-current-file takes file-name

Browse source
This commit is contained in:
Soonho Kong 2014-08-25 16:27:33 -07:00
parent cc1d44e541
commit 5965bcc10b
2 changed files with 25 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -255,6 +255,8 @@
;; NAY Information
;; ----------------
(defun lean-info-nay () '(NAY))
(defun lean-info-nay-type (nay)
(cl-first nay))
(defun lean-info-nay-p (nay)
@ -264,7 +266,7 @@
((pred listp) (and (lean-info-nay-p (cl-first nay))))))
(defun lean-info-nay-parse (seq)
(when (lean-info-nay-p seq)
'(NAY)))
(lean-info-nay)))
;; -- Test
(cl-assert (lean-info-nay-p "-- NAY"))
@ -342,6 +344,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
collect result)))
(defun lean-info-list-filter (info-list start-column)
"Given a info-list, only return an info-item is NAY or whose start-column is matched with the argument."
(--filter (let ((col (lean-info-column it)))
(and col (= start-column col)))
info-list))
@ -413,9 +416,13 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
start-column))))
(defun lean-info-list-parse (str &optional file-name column-number)
"Parse input string and return info-list."
(let ((info-list (lean-info-list-parse-string str))
start-column)
(cond
;; If there is NAY, return it.
((-any? 'lean-info-nay-p info-list)
`(,(lean-info-nay)))
;; When file-name/column-number is specified, try to start-column of id/symbol
((and file-name column-number)
(setq start-column (lean-info-list-find-start-column info-list file-name column-number))
@ -479,7 +486,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
(defun lean-get-info-record (file-name line-number column-number)
"Get info list from lean server using file-name and line-number"
(lean-server-send-cmd (lean-cmd-visit file-name))
(lean-server-check-current-file file-name)
(lean-server-send-cmd (lean-cmd-info line-number))
(while (not lean-global-server-message-to-process)
(accept-process-output (lean-server-get-process) 0 50 t))

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

@ -93,20 +93,21 @@
(setq lean-global-server-current-file-name nil)
(setq lean-global-server-message-to-process nil)
(setq lean-global-server-process lean-server-process)
(message "lean-server process %S created." lean-server-process)
lean-server-process))
(defun lean-server-kill-process ()
"Kill lean-server process. Return t if killed, nil if nothing to kill"
(interactive)
(cond
(lean-global-server-process
(message "lean-server-kill-process: %S killed" lean-global-server-process)
(kill-process lean-global-server-process)
(setq lean-global-server-process nil)
t)
(t (message "lean-server-kill-process: no process to kill")
nil)))
(lean-global-server-process
(when (interactive-p)
(message "lean-server-kill-process: %S killed" lean-global-server-process))
(kill-process lean-global-server-process)
(setq lean-global-server-process nil)
t)
(t (when (interactive-p)
(message "lean-server-kill-process: no process to kill"))
nil)))
(defun lean-server-restart-process ()
"Restart lean-server process."
@ -117,11 +118,11 @@
(defun lean-server-get-process ()
"Get lean-server process. If needed, create a one."
(cond ((not lean-global-server-process)
(message "lean-server-get-process: no process")
(lean-server-create-process))
(lean-server-create-process))
((not (process-live-p lean-global-server-process))
(message "lean-server-get-process: %S is not live, kill it"
lean-global-server-process)
(when (interactive-p)
(message "lean-server-get-process: %S is not live, kill it"
lean-global-server-process))
(lean-server-kill-process))
(t lean-global-server-process)))
@ -139,11 +140,11 @@ Send REPLACE commands to lean-server, reset lean-changed-lines to nil."
do (lean-server-send-cmd (lean-cmd-replace n (lean-grab-line n)))
finally (setq lean-changed-lines nil)))
(defun lean-server-check-current-file ()
(defun lean-server-check-current-file (&optional file-name)
"Check lean-global-server-current-file-name.
If it's not the same with (buffer-file-name), send VISIT cmd."
(let ((current-file-name (buffer-file-name)))
If it's not the same with file-name (default: buffer-file-name), send VISIT cmd."
(let ((current-file-name (or file-name (buffer-file-name))))
(unless (string= lean-global-server-current-file-name
current-file-name)
(lean-server-send-cmd (lean-cmd-visit current-file-name)))))