diff --git a/src/emacs/lean-changes.el b/src/emacs/lean-changes.el new file mode 100644 index 000000000..5d07739ed --- /dev/null +++ b/src/emacs/lean-changes.el @@ -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) diff --git a/src/emacs/lean-cmd.el b/src/emacs/lean-cmd.el index 4e0d90cb2..9c4bc3515 100644 --- a/src/emacs/lean-cmd.el +++ b/src/emacs/lean-cmd.el @@ -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)) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 5bd74c334..1c8b89ebf 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -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. diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 2ec44e898..d6acb2965 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -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 diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index ba7fc54c1..4b452f97a 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -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) diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index 1cebd67f0..5c3893672 100644 --- a/src/emacs/lean-variable.el +++ b/src/emacs/lean-variable.el @@ -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")