max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(shell/server,emacs): show currently executing task if even from another file

Browse source
This commit is contained in:
Gabriel Ebner 2016-12-12 14:09:50 -05:00 • committed by Leonardo de Moura
parent 902df5d134
commit d5bca10af8
2 changed files with 35 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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)

15
src/shell/server.cpp
View file

@ -81,19 +81,34 @@ public:
struct current_tasks_msg {
std::vector<json> m_tasks;
optional<json> 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) {