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

feat(emacs/lean-changes): handle before/after-revert

Browse source
This commit is contained in:
Soonho Kong 2014-09-12 14:22:39 -07:00
parent 27ae03878c
commit 563cfa73ec
6 changed files with 156 additions and 113 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

136
src/emacs/lean-changes.el Normal file
View file

@ -0,0 +1,136 @@
;; -*- lexical-binding: t; -*-
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'dash)
(require 'lean-server)
(require 'lean-debug)
(defvar-local lean-changed-lines nil
"Changed lines")
(defvar-local lean-removed-lines nil
"Removed lines")
(defvar-local lean-inserted-lines nil
"Inserted lines")
(defun lean-before-change-function (beg end)
"Function attached to before-change-functions hook.
It saves the following information to the global variable:
- lean-global-before-change-beg : beg
- lean-global-before-change-end : end
- lean-global-before-change-beg-line-number : line-number of beg
- lean-global-before-change-end-line-number : line-number of end
- lean-global-before-change-text : text between beg and end
These information will be used by lean-after-changed-function."
(lean-server-get-process)
(setq lean-global-before-change-beg beg)
(setq lean-global-before-change-end end)
(setq lean-global-before-change-beg-line-number (line-number-at-pos beg))
(setq lean-global-before-change-end-line-number (line-number-at-pos end))
(setq lean-global-before-change-text (buffer-substring-no-properties beg end)))
(defun lean-after-change-diff-lines (before-beg-line-number
before-end-line-number
after-beg-line-number
after-end-line-number)
"Given before and after (beg-line-number, end-line-number) pairs,
compute changed-lines, inserted-lines, and removed-lines."
(let* ((old-lines (cl-loop for n from before-beg-line-number to before-end-line-number
collect n))
(new-lines (cl-loop for n from after-beg-line-number to after-end-line-number
collect n))
(old-lines-len (length old-lines))
(new-lines-len (length new-lines))
changed-lines removed-lines inserted-lines)
(cond ((= old-lines-len new-lines-len)
(setq changed-lines old-lines)
`(CHANGE-ONLY ,changed-lines))
;; Case "REMOVE"
((> old-lines-len new-lines-len)
(setq removed-lines (-take (- old-lines-len new-lines-len) old-lines))
;; Make sure that we return it in reverse order
(setq removed-lines (cl-sort removed-lines '>))
(setq changed-lines new-lines)
`(REMOVE ,removed-lines ,changed-lines))
;; Case "INSERT"
((< old-lines-len new-lines-len)
(setq inserted-lines (-drop old-lines-len new-lines))
;; Make sure that we return it in sorted order
(setq inserted-lines (cl-sort inserted-lines '<))
(setq changed-lines old-lines)
`(INSERT ,inserted-lines ,changed-lines)))))
(defun lean-after-changed-p (before-beg before-end before-text
after-beg after-end after-text)
"Return true if there is a really change"
(or (/= before-beg after-beg)
(/= before-end after-end)
(not (string= before-text after-text))))
(defun lean-after-change-handle-changes-only (changed-lines)
(cl-loop for n in changed-lines
do (add-to-list 'lean-changed-lines n)))
(defun lean-after-change-handle-inserted (inserted-lines changed-lines)
(lean-server-flush-changed-lines)
(cl-loop for n in inserted-lines
do (lean-server-send-cmd-async (lean-cmd-insert n (lean-grab-line n))))
(setq lean-changed-lines changed-lines)
(lean-server-flush-changed-lines))
(defun lean-after-change-handle-removed (removed-lines changed-lines)
(lean-server-flush-changed-lines)
(cl-loop for n in removed-lines
do (lean-server-send-cmd-async (lean-cmd-remove n)))
(setq lean-changed-lines changed-lines)
(lean-server-flush-changed-lines))
(defun lean-after-change-function (beg end leng-before)
"Function attached to after-change-functions hook"
(let* ((before-beg lean-global-before-change-beg)
(before-end lean-global-before-change-end)
(before-beg-line-number lean-global-before-change-beg-line-number)
(before-end-line-number lean-global-before-change-end-line-number)
(after-beg-line-number (line-number-at-pos beg))
(after-end-line-number (line-number-at-pos end))
(before-text lean-global-before-change-text)
(text (buffer-substring-no-properties beg end)))
(lean-debug "after-change-function")
(lean-debug "before-text: %s" before-text)
(lean-debug "after-text: %s" text)
(when (lean-after-changed-p before-beg before-end before-text
beg end text)
(pcase (lean-after-change-diff-lines before-beg-line-number before-end-line-number
after-beg-line-number after-end-line-number)
(`(CHANGE-ONLY ,changed-lines)
(lean-after-change-handle-changes-only changed-lines))
(`(INSERT ,inserted-lines ,changed-lines)
(lean-after-change-handle-inserted inserted-lines changed-lines))
(`(REMOVE ,removed-lines ,changed-lines)
(lean-after-change-handle-removed removed-lines changed-lines))))))
(defconst lean-changes-hooks-alist
'((after-change-functions . lean-after-change-function)
(before-change-functions . lean-before-change-function)))
(defun lean-before-revert ()
"Remove changes hooks"
(pcase-dolist (`(,hook . ,fn) lean-changes-hooks-alist)
(remove-hook hook fn 'local)))
(defun lean-after-revert ()
"Reset changes variables, add back changes-hooks, load file"
(setq lean-changed-lines nil)
(setq lean-removed-lines nil)
(setq lean-inserted-lines nil)
(pcase-dolist (`(,hook . ,fn) lean-changes-hooks-alist)
(add-hook hook fn nil 'local))
(lean-server-send-cmd-async (lean-cmd-load (buffer-file-name))))
(provide 'lean-changes)

4
src/emacs/lean-cmd.el
View file

@ -36,7 +36,9 @@ remaining commands are all with respect to the current file. If
it. Some of the remaining commands apply 'changes' to the current
file. The LOAD command can be used to discard all these changes,
and enforce the content of the file stored in file system."
`(VISIT ,(or file-name (buffer-file-name))))
(let ((file-name (or file-name (buffer-file-name))))
(cl-assert file-name)
`(VISIT ,file-name)))
(defun lean-cmd-visit-get-file-name (visit-cmd)
(cl-second visit-cmd))

6
src/emacs/lean-mode.el
View file

@ -25,6 +25,7 @@
(require 'lean-syntax)
(require 'lean-mmm-lua)
(require 'lean-company)
(require 'lean-changes)
(require 'lean-server)
(require 'lean-project)
@ -121,15 +122,14 @@
;; ;; clean up temporary files and directories.
;; (kill-buffer-hook . lean-teardown)
;; (change-major-mode-hook . lean-teardown)
;; (before-revert-hook . lean-teardown)
(before-revert-hook . lean-before-revert)
(after-revert-hook . lean-after-revert)
;; ;; Update the error list if necessary
;; (post-command-hook . lean-error-list-update-source)
;; (post-command-hook . lean-error-list-highlight-errors)
;; ;; Show or hide error popups after commands
;; (post-command-hook . lean-display-error-at-point-soon)
;; (post-command-hook . lean-hide-error-buffer)
;; ;; Immediately show error popups when navigating to an error
;; (next-error-hook . lean-display-error-at-point))
)
"Hooks which lean-mode needs to hook in.

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

@ -167,7 +167,7 @@
(set-process-query-on-exit-flag lean-server-process nil)
(lean-server-initialize-global-vars)
(setq lean-global-server-process lean-server-process)
(lean-debug "lean-server process created")
(lean-debug "lean-server process %S is created" lean-server-process)
lean-server-process))
(defun lean-server-kill-process ()
@ -193,6 +193,12 @@
(and (lean-server-kill-process)
(lean-server-create-process)))
(defun lean-server-process-exist-p ()
"Return t if lean-server-process exists, otherwise return nil"
(if lean-global-server-process
t
nil))
(defun lean-server-get-process ()
"Get lean-server process. If needed, create a one."
(cond ((not lean-global-server-process)
@ -219,11 +225,11 @@ Send REPLACE commands to lean-server, reset lean-changed-lines to nil."
finally (setq lean-changed-lines nil)))
(defun lean-server-visit-current-buffer ()
"Send VISIT for the current buffer"
(cond ((and (buffer-modified-p)
(not lean-global-server-current-file-name))
(lean-server-handle-modified-buffer))
(t
(lean-server-send-cmd-async (lean-cmd-visit)))))
(t (lean-server-send-cmd-async (lean-cmd-visit)))))
(defun lean-server-check-current-file (&optional file-name)
"Check lean-global-server-current-file-name

100
src/emacs/lean-type.el
View file

@ -12,6 +12,7 @@
(require 'lean-util)
(require 'lean-cmd)
(require 'lean-server)
(require 'lean-changes)
(require 'lean-debug)
(require 'flymake)
@ -70,103 +71,4 @@
(call-process (lean-get-executable "linja") nil 0 nil "clear-cache")
(lean-server-send-cmd-async (lean-cmd-clear-cache)))
;; =======================================================
;; Change Handling
;; =======================================================
(defun lean-before-change-function (beg end)
"Function attached to before-change-functions hook.
It saves the following information to the global variable:
- lean-global-before-change-beg : beg
- lean-global-before-change-end : end
- lean-global-before-change-beg-line-number : line-number of beg
- lean-global-before-change-end-line-number : line-number of end
- lean-global-before-change-text : text between beg and end
These information will be used by lean-after-changed-function."
(lean-server-get-process)
(setq lean-global-before-change-beg beg)
(setq lean-global-before-change-end end)
(setq lean-global-before-change-beg-line-number (line-number-at-pos beg))
(setq lean-global-before-change-end-line-number (line-number-at-pos end))
(setq lean-global-before-change-text (buffer-substring-no-properties beg end)))
(defun lean-after-change-diff-lines (before-beg-line-number
before-end-line-number
after-beg-line-number
after-end-line-number)
"Given before and after (beg-line-number, end-line-number)
pairs, compute changed-lines, inserted-lines, and removed-lines."
(let* ((old-lines (cl-loop for n from before-beg-line-number to before-end-line-number
collect n))
(new-lines (cl-loop for n from after-beg-line-number to after-end-line-number
collect n))
(old-lines-len (length old-lines))
(new-lines-len (length new-lines))
changed-lines removed-lines inserted-lines)
(cond ((= old-lines-len new-lines-len)
(setq changed-lines old-lines)
`(CHANGE-ONLY ,changed-lines))
;; Case "REMOVE"
((> old-lines-len new-lines-len)
(setq removed-lines (-take (- old-lines-len new-lines-len) old-lines))
;; Make sure that we return it in reverse order
(setq removed-lines (cl-sort removed-lines '>))
(setq changed-lines new-lines)
`(REMOVE ,removed-lines ,changed-lines))
;; Case "INSERT"
((< old-lines-len new-lines-len)
(setq inserted-lines (-drop old-lines-len new-lines))
;; Make sure that we return it in sorted order
(setq inserted-lines (cl-sort inserted-lines '<))
(setq changed-lines old-lines)
`(INSERT ,inserted-lines ,changed-lines)))))
(defun lean-after-changed-p (before-beg before-end after-beg after-end
before-text after-text)
"Return true if there is a really change"
(or (/= before-beg after-beg)
(/= before-end after-end)
(not (string= before-text after-text))))
(defun lean-after-change-handle-changes-only (changed-lines)
(cl-loop for n in changed-lines
do (add-to-list 'lean-changed-lines n)))
(defun lean-after-change-handle-inserted (inserted-lines changed-lines)
(lean-server-flush-changed-lines)
(cl-loop for n in inserted-lines
do (lean-server-send-cmd-async (lean-cmd-insert n (lean-grab-line n))))
(setq lean-changed-lines changed-lines)
(lean-server-flush-changed-lines))
(defun lean-after-change-handle-removed (removed-lines changed-lines)
(lean-server-flush-changed-lines)
(cl-loop for n in removed-lines
do (lean-server-send-cmd-async (lean-cmd-remove n)))
(setq lean-changed-lines changed-lines)
(lean-server-flush-changed-lines))
(defun lean-after-change-function (beg end leng-before)
"Function attached to after-change-functions hook"
(let* ((before-beg lean-global-before-change-beg)
(before-end lean-global-before-change-end)
(before-beg-line-number lean-global-before-change-beg-line-number)
(before-end-line-number lean-global-before-change-end-line-number)
(after-beg-line-number (line-number-at-pos beg))
(after-end-line-number (line-number-at-pos end))
(before-text lean-global-before-change-text)
(after-text (buffer-substring-no-properties beg end)))
(when (lean-after-changed-p before-beg before-end beg end before-text after-text)
(pcase (lean-after-change-diff-lines before-beg-line-number before-end-line-number
after-beg-line-number after-end-line-number)
(`(CHANGE-ONLY ,changed-lines)
(lean-after-change-handle-changes-only changed-lines))
(`(INSERT ,inserted-lines ,changed-lines)
(lean-after-change-handle-inserted inserted-lines changed-lines))
(`(REMOVE ,removed-lines ,changed-lines)
(lean-after-change-handle-removed removed-lines changed-lines))))))
(provide 'lean-type)

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

@ -39,21 +39,18 @@ where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | FINDP | FINDG | ERROR,
(defvar lean-global-async-task-queue nil
"Tasks (continuations) to be executed.")
(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")