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

perf(shell/server,emacs): do not actually compute completions during preliminary 'complete' requests

Browse source
This commit is contained in:
Sebastian Ullrich 2016-12-27 20:37:12 +01:00 • committed by Leonardo de Moura
parent d228c24c81
commit 3e2d1de21a
3 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/emacs/lean-company.el
View file

@ -38,14 +38,15 @@
(cond ((s-prefix? prefix candidate) candidates)
(t `(,candidate ,prefix)))))
(defun company-lean--exec ()
(cl-defun company-lean--exec (&key skip-completions)
"Synchronously queries completions for the current point from server and returns a plist with keys :prefix and :candidates., or nil if no completion should be triggered."
(lean-server-sync)
(let* ((col (lean-line-offset))
(response (lean-server-send-synchronous-command
'complete (list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column col)))
:column col
:skip_completions (or skip-completions :json-false))))
(candidates (plist-get response :completions))
(prefix (plist-get response :prefix)))
(when candidates
@ -92,7 +93,7 @@
(defun company-lean (command &optional arg &rest ignored)
(cl-case command
(prefix (plist-get (company-lean--exec) :prefix))
(prefix (plist-get (company-lean--exec :skip-completions t) :prefix))
(candidates (plist-get (company-lean--exec) :candidates))
(annotation (company-lean--annotation arg))
;(location (cons :async (lambda (cb) (company-lean--findp-location arg cb))))

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

@ -75,7 +75,7 @@
(interactive)
(if (minibufferp)
(minibuffer-complete)
(cond ((and lean-company-use (company-lean--exec))
(cond ((and lean-company-use (company-lean--exec :skip-completions t))
(company-complete-common))
(lean-company-use (lean-tab-indent))
((lean-check-expansion)

14
src/shell/server.cpp
View file

@ -322,10 +322,12 @@ class server::auto_complete_task : public task<unit> {
server * m_server;
unsigned m_seq_num;
std::shared_ptr<module_info const> m_mod_info;
bool m_skip_completions;
public:
auto_complete_task(server * server, unsigned seq_num, std::shared_ptr<module_info const> const & mod_info) :
m_server(server), m_seq_num(seq_num), m_mod_info(mod_info) {}
auto_complete_task(server * server, unsigned seq_num, std::shared_ptr<module_info const> const & mod_info,
bool skip_completions) :
m_server(server), m_seq_num(seq_num), m_mod_info(mod_info), m_skip_completions(skip_completions) {}
// TODO(gabriel): find cleaner way to give it high prio
task_kind get_kind() const override { return task_kind::parse; }
@ -355,7 +357,8 @@ public:
std::string prefix = e.m_token->to_string();
if (auto stop = utf8_char_pos(prefix.c_str(), get_pos().second - e.m_token_pos->second))
prefix = prefix.substr(0, *stop);
j["completions"] = get_completions(prefix, snap->m_env, snap->m_options);
if (!m_skip_completions)
j["completions"] = get_completions(prefix, snap->m_env, snap->m_options);
j["prefix"] = prefix;
}
} catch (throwable & ex) {}
@ -372,13 +375,16 @@ public:
void server::handle_complete(cmd_req const & req) {
std::string fn = req.m_payload.at("file_name");
pos_info pos = {req.m_payload.at("line"), req.m_payload.at("column")};
bool skip_completions = false;
if (req.m_payload.count("skip_completions"))
skip_completions = req.m_payload.at("skip_completions");
scope_message_context scope_msg_ctx(message_bucket_id { "_server", 0 });
scoped_task_context scope_task_ctx(fn, pos);
auto mod_info = m_mod_mgr->get_module(fn);
get_global_task_queue()->submit<auto_complete_task>(this, req.m_seq_num, mod_info);
get_global_task_queue()->submit<auto_complete_task>(this, req.m_seq_num, mod_info, skip_completions);
}
class server::info_task : public task<unit> {