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

perf(frontends/lean/parser): break at break_at_pos even if not on an interesting token

Browse source
This commit is contained in:
Sebastian Ullrich 2016-12-27 12:24:29 +01:00 • committed by Leonardo de Moura
parent 47e7df9b27
commit 5cb06ea912
3 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser.cpp
View file

@ -203,7 +203,9 @@ bool parser::check_break_at_pos(pos_info const & p, name const & tk) {
void parser::scan() {
if (curr_is_identifier() && check_break_at_pos(pos(), get_name_val()))
throw break_at_pos_exception(pos(), get_name_val());
throw info_at_pos_exception(pos(), get_name_val());
if (m_break_at_pos && *m_break_at_pos < pos())
throw break_at_pos_exception();
m_curr = m_scanner.scan(m_env);
}
@ -1245,7 +1247,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
auto check_break = [&]() {
if (check_break_at_pos(pos(), get_token_info().value())) {
// info is stored at position of first notation token
throw break_at_pos_exception(p, first_token);
throw info_at_pos_exception(p, first_token);
}
};
buffer<expr> args;

6
src/frontends/lean/parser.h
View file

@ -77,12 +77,14 @@ struct snapshot {
typedef std::vector<std::shared_ptr<snapshot const>> snapshot_vector;
class break_at_pos_exception : public std::exception {
class break_at_pos_exception : public std::exception {};
class info_at_pos_exception : public break_at_pos_exception {
public:
pos_info m_token_pos;
name m_token;
break_at_pos_exception(pos_info const & token_pos, name const & token):
info_at_pos_exception(pos_info const & token_pos, name const & token):
m_token_pos(token_pos), m_token(token) {}
};

4
src/shell/server.cpp
View file

@ -391,7 +391,7 @@ public:
use_exceptions, std::make_shared<snapshot>(s), nullptr);
p.set_break_at_pos(pos);
p();
} catch (break_at_pos_exception & e) {
} catch (info_at_pos_exception & e) {
lean_assert(e.m_token_pos.first == pos.first);
auto opts = m_server->m_ios.get_options();
@ -411,7 +411,7 @@ public:
}
j["record"] = record;
}
} catch (break_at_pos_exception & e) {}
}
m_server->send_msg(cmd_res(m_seq_num, j));