michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/server): add timebound to WAIT command, closes #156

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-09 10:28:11 -07:00
parent dab9ef31e3
commit 53292d8297
2 changed files with 33 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/frontends/lean/server.cpp
View file

@ -232,12 +232,20 @@ void server::worker::request_interrupt() {
m_thread.request_interrupt();
}
void server::worker::wait() {
bool server::worker::wait(optional<unsigned> const & ms) {
while (true) {
unique_lock<mutex> lk(m_todo_mutex);
if (!m_todo_file)
break;
m_todo_cv.wait(lk);
return true;
if (ms) {
chrono::milliseconds d(*ms);
m_todo_cv.wait_for(lk, d);
if (!m_todo_file)
return true;
return false;
} else {
m_todo_cv.wait(lk);
}
}
}
@ -361,6 +369,16 @@ unsigned consume_num(std::string const & data, unsigned & i) {
return r;
}
optional<unsigned> server::get_optional_num(std::string const & line, std::string const & cmd) {
std::string data = line.substr(cmd.size());
unsigned i = 0;
consume_spaces(data, i);
if (i == data.size())
return optional<unsigned>();
unsigned r = consume_num(data, i);
return optional<unsigned>(r);
}
void check_line_num(unsigned line_num) {
if (line_num == 0)
throw exception("line numbers are indexed from 1");
@ -740,6 +758,13 @@ void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string
m_out << "-- ENDFINDG" << std::endl;
}
void server::wait(optional<unsigned> ms) {
m_out << "-- BEGINWAIT" << std::endl;
if (!m_worker.wait(ms))
m_out << "-- INTERRUPTED\n";
m_out << "-- ENDWAIT" << std::endl;
}
bool server::operator()(std::istream & in) {
for (std::string line; std::getline(in, line);) {
try {
@ -779,9 +804,8 @@ bool server::operator()(std::istream & in) {
} else if (is_command(g_options, line)) {
show_options();
} else if (is_command(g_wait, line)) {
m_out << "-- BEGINWAIT" << std::endl;
m_worker.wait();
m_out << "-- ENDWAIT" << std::endl;
optional<unsigned> ms = get_optional_num(line, g_wait);
wait(ms);
} else if (is_command(g_show, line)) {
show(false);
} else if (is_command(g_valid, line)) {

4
src/frontends/lean/server.h
View file

@ -57,7 +57,7 @@ class server {
~worker();
void set_todo(file_ptr const & f, unsigned line_num, options const & o);
void request_interrupt();
void wait();
bool wait(optional<unsigned> const & ms);
};
file_map m_file_map;
@ -89,7 +89,9 @@ class server {
void interrupt_worker();
void show_options();
void show(bool valid);
void wait(optional<unsigned> ms);
unsigned get_line_num(std::string const & line, std::string const & cmd);
optional<unsigned> get_optional_num(std::string const & line, std::string const & cmd);
pair<unsigned, optional<unsigned>> get_line_opt_col_num(std::string const & line, std::string const & cmd);
pair<unsigned, unsigned> get_line_col_num(std::string const & line, std::string const & cmd);
void find_goal_matches(unsigned line_num, unsigned col_num, std::string const & filters);