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

feat(frontends/lean/server): ingore keywords and commands in FINDP

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-05 20:59:14 -07:00
parent b5f595c432
commit 629feb77ef
3 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -533,6 +533,12 @@ void server::find_pattern(unsigned line_num, std::string const & pattern) {
m_out << " STALE";
environment const & env = env_opts->first;
options opts = env_opts->second;
token_table const & tt = get_token_table(env);
if (is_token(tt, pattern.c_str())) {
// we ignore patterns that match commands, keywords, and tokens.
m_out << "\n-- ENDFINDP" << std::endl;
return;
}
opts = join(opts, m_ios.get_options());
m_out << std::endl;
unsigned max_errors = get_fuzzy_match_max_errors(pattern.size());

3
src/frontends/lean/token_table.cpp
View file

@ -38,6 +38,9 @@ optional<unsigned> get_precedence(token_table const & s, char const * token) {
auto it = find(s, token);
return it ? optional<unsigned>(it->precedence()) : optional<unsigned>();
}
bool is_token(token_table const & s, char const * token) {
return static_cast<bool>(find(s, token));
}
void for_each(token_table const & s, std::function<void(char const *, token_info const &)> const & fn) {
s.for_each([&](unsigned num, char const * keys, token_info const & info) {
buffer<char> str;

1
src/frontends/lean/token_table.h
View file

@ -46,6 +46,7 @@ void for_each(token_table const & s, std::function<void(char const *, token_info
void display(std::ostream & out, token_table const & s);
token_table const * find(token_table const & s, char c);
optional<unsigned> get_precedence(token_table const & s, char const * token);
bool is_token(token_table const & s, char const * token);
token_info const * value_of(token_table const & s);
void open_token_table(lua_State * L);
}