feat(emacs,shell/server): add different region-of-interest options

src/emacs/lean-mode.el

@@ -91,6 +91,10 @@
 (defvar lean-mode-map (make-sparse-keymap)
   "Keymap used in Lean mode")
 
+(defun lean-mk-check-menu-option (text sym)
+  `[,text (progn (setq lean-server-check-mode ',sym) (lean-server-sync-roi))
+         :style radio :selected (eq lean-server-check-mode ',sym)])
+
 (easy-menu-define lean-mode-menu lean-mode-map
   "Menu for the Lean major mode"
   `("Lean"
@@ -108,9 +112,11 @@
     "-----------------"
     ["Restart lean process" lean-server-restart               t]
     "-----------------"
+    ,(lean-mk-check-menu-option "Check nothing" 'nothing)
+    ,(lean-mk-check-menu-option "Check visible lines" 'visible-lines)
+    ,(lean-mk-check-menu-option "Check visible files" 'visible-files)
+    "-----------------"
     ("Configuration"
-     ["Use flycheck (on-the-fly syntax check)"
-      lean-toggle-flycheck-mode :active t :style toggle :selected flycheck-mode]
      ["Show type at point"
       lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
     "-----------------"

src/emacs/lean-server.el

@@ -121,7 +121,7 @@
                 :project-dir project-dir
                 :process proc
                 :seq-num 0
-                :current-roi nil
+                :current-roi 'not-yet-sent
                 :callbacks nil
                 :messages nil)))
     (set-process-filter proc (lambda (proc string) (lean-server-filter sess string)))
@@ -292,6 +292,8 @@
     (setq lean-server-session (lean-server-session-get
                                (or (lean-project-find-root)
                                    (file-name-directory (buffer-file-name)))))
+    (lean-server-show-tasks)
+    (lean-server-show-messages)
     (lean-server-sync)))
 
 (defun lean-server-restart ()
@@ -336,15 +338,25 @@
           (run-at-time "200 milliseconds" nil #'lean-server-sync (current-buffer)))))
 
 (defun lean-server-compute-roi (sess)
-  (-mapcat (lambda (buf)
-             (with-current-buffer buf
-               (when (and (get-buffer-window) (eq lean-server-session sess))
-                 (let ((min-pt (-min (--map (window-start it) (get-buffer-window-list))))
-                       (max-pt (-max (--map (window-end it t) (get-buffer-window-list)))))
+  (pcase lean-server-check-mode
+    ('visible-lines
+     (-mapcat (lambda (buf)
+                (with-current-buffer buf
+                  (when (and (get-buffer-window) (eq lean-server-session sess))
+                    (let ((min-pt (-min (--map (window-start it) (get-buffer-window-list))))
+                          (max-pt (-max (--map (window-end it t) (get-buffer-window-list)))))
+                      `((,(buffer-file-name)
+                         ,(max 1 (- (line-number-at-pos min-pt) 5)) .
+                         ,(+ (line-number-at-pos max-pt) 5)))))))
+              (buffer-list)))
+    ('visible-files
+     (--mapcat (with-current-buffer it
+                 (when (and (get-buffer-window) (eq lean-server-session sess))
                    `((,(buffer-file-name)
-                      ,(max 1 (- (line-number-at-pos min-pt) 5)) .
-                      ,(+ (line-number-at-pos max-pt) 5)))))))
-           (buffer-list)))
+                      ,(line-number-at-pos (point-min)) .
+                      ,(line-number-at-pos (point-max))))))
+               (buffer-list)))
+    (_ nil)))
 
 (defun lean-server-session-send-roi (sess roi)
   (setf (lean-server-session-current-roi sess) roi)
@@ -361,15 +373,24 @@
                  (<= (cddr it) (cdr b))))
           as))
 
+(defun lean-server-roi-extend (roi delta)
+  (--map `(,(car it) ,(- (cadr it) delta) . ,(+ (cddr it) delta)) roi))
+
+(defun lean-server-roi-ok (old-roi new-roi)
+  (and (lean-server-roi-subset-p new-roi old-roi)
+       (lean-server-roi-subset-p old-roi (lean-server-roi-extend new-roi 10))))
+
 (defun lean-server-sync-roi ()
-  (let ((old-roi (lean-server-session-current-roi lean-server-session))
-        (new-roi (lean-server-compute-roi lean-server-session)))
-    (when (not (lean-server-roi-subset-p new-roi old-roi))
-      (lean-server-session-send-roi lean-server-session new-roi))))
+  (when lean-server-session
+    (let ((old-roi (lean-server-session-current-roi lean-server-session))
+          (new-roi (lean-server-compute-roi lean-server-session)))
+      (when (or (eq old-roi 'not-yet-sent) (not (lean-server-roi-ok old-roi new-roi)))
+        (lean-server-session-send-roi lean-server-session new-roi)))))
 
 (defun lean-server-window-scroll-function-hook (wnd new-start-pos)
   (let ((buf (window-buffer wnd)))
     (with-current-buffer buf
-      (when lean-server-session (lean-server-sync-roi)))))
+      (lean-server-ensure-alive)
+      (lean-server-sync-roi))))
 
 (provide 'lean-server)

src/emacs/lean-settings.el

@@ -93,6 +93,12 @@ false (nil)."
   :group 'lean
   :type 'boolean)
 
+(defcustom lean-server-check-mode 'visible-lines
+  "What parts of the open files the Lean server should check"
+  :group 'lean
+  :type 'symbol
+  :options '(nothing visible-lines visible-files))
+
 (defcustom lean-keybinding-std-exe1 (kbd "C-c C-x")
   "Lean Keybinding for std-exe #1"
   :group 'lean-keybinding :type 'key-sequence)

src/emacs/lean-type.el

@@ -110,10 +110,11 @@
 (defun lean-eldoc-documentation-function (&optional add-to-kill-ring)
   "Show information of lean expression at point if any"
   (interactive)
-  (lean-get-info-record-at-point
-   (lambda (info-record)
-     (when info-record
-       (lean-eldoc-documentation-function-cont info-record add-to-kill-ring)))))
+  (when (not (eq lean-server-check-mode 'nothing)) ; TODO(gabriel): revisit once info no longer reparses the file
+    (lean-get-info-record-at-point
+     (lambda (info-record)
+       (when info-record
+         (lean-eldoc-documentation-function-cont info-record add-to-kill-ring))))))
 
 (defun lean-show-type ()
   "Show information of lean-expression at point if any."
@@ -124,7 +125,9 @@
 
 (defun lean-show-goal--handler ()
   (let ((deactivate-mark)) ; keep transient mark
-    (when (lean-info-buffer-active lean-show-goal-buffer-name)
+    (when (and (not (eq lean-server-check-mode 'nothing))
+               ; TODO(gabriel): revisit ^^ once info no longer reparses the file
+               (lean-info-buffer-active lean-show-goal-buffer-name))
       (lean-get-info-record-at-point
        (lambda (info-record)
          (lean-with-info-output-to-buffer

src/library/mt_task_queue.cpp

@@ -112,7 +112,9 @@ void mt_task_queue::spawn_worker() {
 void mt_task_queue::handle_finished(gtask const & t) {
     lean_assert(get_state(t).load() > task_state::Running);
     lean_assert(get_data(t));
-    lean_assert(get_data(t)->m_sched_info);
+
+    if (!get_data(t)->m_sched_info)
+        return;  // task has never been submitted
 
     m_waiting.erase(t);
     get_sched_info(t).m_has_finished.notify_all();

src/shell/server.cpp

@@ -51,7 +51,7 @@ struct all_messages_msg {
 };
 
 bool region_of_interest::intersects(log_tree::node const & n) const {
-    if (m_files.empty()) return true;
+    if (!m_enabled) return true;
     if (n.get_location().m_file_name.empty()) return true;
     auto & l = n.get_location();
     if (auto f = m_files.find(l.m_file_name)) {
@@ -63,7 +63,7 @@ bool region_of_interest::intersects(log_tree::node const & n) const {
 }
 
 bool region_of_interest::intersects(message const & msg) const {
-    if (m_files.empty()) return true;
+    if (!m_enabled) return true;
     if (auto f = m_files.find(msg.get_file_name())) {
         return f->m_begin_line <= msg.get_pos().first && msg.get_pos().first <= f->m_end_line;
     } else {
@@ -87,7 +87,7 @@ public:
 
     std::vector<message> get_messages_core(region_of_interest const & roi) {
         std::vector<message> msgs;
-        m_lt->get_root().for_each([&] (log_tree::node const & n) {
+        m_lt->for_each([&] (log_tree::node const & n) {
             if (roi.intersects(n)) {
                 for (auto & e : n.get_entries()) {
                     if (auto msg = dynamic_cast<message const *>(e.get())) {
@@ -599,6 +599,7 @@ region_of_interest server::get_roi() {
 
 server::cmd_res server::handle_roi(server::cmd_req const & req) {
     region_of_interest new_roi;
+    new_roi.m_enabled = true;
     for (auto & f : req.m_payload.at("files")) {
         std::string fn = f.at("file_name");
         unsigned begin_line = f.at("begin_line");

src/shell/server.h

@@ -31,6 +31,7 @@ struct string_cmp {
 };
 
 struct region_of_interest {
+    bool m_enabled = false;
     rb_map<std::string, line_range, string_cmp> m_files;
 
     bool intersects(log_tree::node const & n) const;