diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el index 7be74fc4ac..2233a9582b 100644 --- a/src/emacs/lean-flycheck.el +++ b/src/emacs/lean-flycheck.el @@ -17,23 +17,32 @@ (flycheck-mode (flycheck-mode -1)) (t (flycheck-mode 1)))) -(cl-defun lean-flycheck-parse-task (checker buffer &key pos_line pos_col desc file_name &allow-other-keys) - (flycheck-error-new-at pos_line (1+ pos_col) - 'info - (format "still running: %s" desc) - :filename file_name - :checker checker :buffer buffer)) +(cl-defun lean-flycheck-parse-task (checker buffer cur-file-name + &key pos_line pos_col desc file_name &allow-other-keys) + (if (equal cur-file-name file_name) + (flycheck-error-new-at pos_line (1+ pos_col) + 'info + (format "still running: %s" desc) + :filename file_name + :checker checker :buffer buffer) + (flycheck-error-new-at 1 1 + 'info + (format "still running: %s" desc) + :filename cur-file-name + :checker checker :buffer buffer))) (defun lean-flycheck-mk-task-msgs (checker buffer sess) (if (and sess (lean-server-session-tasks sess) (plist-get (lean-server-session-tasks sess) :is_running)) (let* ((cur-fn (buffer-file-name)) + (tasks (lean-server-session-tasks sess)) + (cur-task (plist-get tasks :cur_task)) (tasks-for-cur-file (remove-if-not (lambda (task) (equal cur-fn (plist-get task :file_name))) - (plist-get (lean-server-session-tasks lean-server-session) :tasks)))) - (if tasks-for-cur-file - (mapcar (lambda (task) (apply #'lean-flycheck-parse-task checker buffer task)) tasks-for-cur-file) - (list (flycheck-error-new-at 1 1 'info "still running: lean error check" - :checker checker :buffer buffer)))))) + (plist-get tasks :tasks)))) + (mapcar (lambda (task) (apply #'lean-flycheck-parse-task checker buffer cur-fn task)) + (if (and tasks-for-cur-file (equal cur-fn (plist-get cur-task :file_name))) + tasks-for-cur-file + (cons cur-task tasks-for-cur-file)))))) (cl-defun lean-flycheck-parse-error (checker buffer &key pos_line pos_col severity text file_name &allow-other-keys) (flycheck-error-new-at pos_line (1+ pos_col) diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 5d3a0ee264..317727ed92 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -81,19 +81,34 @@ public: struct current_tasks_msg { std::vector m_tasks; + optional m_cur_task; bool m_is_running = false; json to_json_response() const { json j; j["response"] = "current_tasks"; j["is_running"] = m_is_running; + if (m_cur_task) j["cur_task"] = *m_cur_task; j["tasks"] = m_tasks; return j; } + json json_of_task(generic_task const * t) { + json j; + j["file_name"] = t->get_module_id(); + auto pos = t->get_pos(); + j["pos_line"] = pos.first; + j["pos_col"] = pos.second; + j["desc"] = t->description(); + return j; + } + #if defined(LEAN_MULTI_THREAD) current_tasks_msg(mt_tq_status const & st, std::string const & visible_file) { m_is_running = st.size() > 0; + if (!st.m_executing.empty()) { + m_cur_task = { json_of_task(st.m_executing.front()) }; + } st.for_each([&] (generic_task const * t) { if (m_tasks.size() >= 100) return; if (!t->is_tiny() && t->get_module_id() == visible_file) {