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

feat(shell/server): add "hole" server command skeleton

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-14 11:44:32 -07:00
parent 55c8627f2c
commit c0556df2ec
2 changed files with 41 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/shell/server.cpp
View file

@ -437,6 +437,8 @@ void server::handle_request(server::cmd_req const & req) {
handle_async_response(req, handle_complete(req));
} else if (command == "info") {
handle_async_response(req, handle_info(req));
} else if (command == "hole") {
handle_async_response(req, handle_hole(req));
} else if (command == "search") {
send_msg(handle_search(req));
} else if (command == "roi") {
@ -617,6 +619,43 @@ task<server::cmd_res> server::handle_info(server::cmd_req const & req) {
.set_cancellation_token(m_bg_task_ctok).build();
}
json server::hole_command(std::shared_ptr<module_info const> const & /* mod_info */, std::string const & /* action */,
pos_info const & pos) {
json j;
std::vector<info_manager> im = get_info_managers(m_lt);
j["message"] = "HOLE!!!!";
j["replacements"]["file"] = "f";
j["replacements"]["start"]["line"] = pos.first;
j["replacements"]["start"]["column"] = pos.second;
j["replacements"]["end"]["line"] = pos.first;
j["replacements"]["end"]["column"] = pos.second + 4;
json r1;
r1["code"] = "(1 + 1)";
r1["description"] = "this is a dummy replacement";
json r2;
r2["code"] = "(2 + 1)";
r2["description"] = "this is another dummy replacement";
j["replacements"]["alternatives"] = {r1, r2};
// TODO(Leo)
return j;
}
task<server::cmd_res> server::handle_hole(cmd_req const & req) {
cancel(m_bg_task_ctok);
m_bg_task_ctok = mk_cancellation_token();
std::string action = req.m_payload.at("action");
std::string fn = req.m_payload.at("file_name");
pos_info pos = {req.m_payload.at("line"), req.m_payload.at("column")};
auto mod_info = m_mod_mgr->get_module(fn);
return task_builder<cmd_res>([=] { return cmd_res(req.m_seq_num, hole_command(mod_info, action, pos)); })
.wrap(library_scopes(log_tree::node()))
.set_cancellation_token(m_bg_task_ctok)
.build();
}
server::cmd_res server::handle_search(server::cmd_req const & req) {
std::string query = req.m_payload.at("query");

2
src/shell/server.h
View file

@ -97,10 +97,12 @@ class server : public module_vfs {
cmd_res handle_sync(cmd_req const & req);
task<cmd_res> handle_complete(cmd_req const & req);
task<cmd_res> handle_info(cmd_req const & req);
task<cmd_res> handle_hole(cmd_req const & req);
cmd_res handle_search(cmd_req const & req);
cmd_res handle_roi(cmd_req const & req);
json autocomplete(std::shared_ptr<module_info const> const & mod_info, bool skip_completions, pos_info const & pos);
json hole_command(std::shared_ptr<module_info const> const & mod_info, std::string const & action, pos_info const & pos);
json info(std::shared_ptr<module_info const> const & mod_info, pos_info const & pos);
public: