diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 877583bf3..696ef9ed9 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -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()); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index fbfbb0c1e..1de18d6b9 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -38,6 +38,9 @@ optional get_precedence(token_table const & s, char const * token) { auto it = find(s, token); return it ? optional(it->precedence()) : optional(); } +bool is_token(token_table const & s, char const * token) { + return static_cast(find(s, token)); +} void for_each(token_table const & s, std::function const & fn) { s.for_each([&](unsigned num, char const * keys, token_info const & info) { buffer str; diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h index 068ccab7c..a7527e359 100644 --- a/src/frontends/lean/token_table.h +++ b/src/frontends/lean/token_table.h @@ -46,6 +46,7 @@ void for_each(token_table const & s, std::function 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); }