From 8e9f97e95e806318c9e554aaa436e793e90c23c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Oct 2014 17:38:59 -0700 Subject: [PATCH] fix(frontends/lean): do not save identifier info --- src/frontends/lean/info_manager.cpp | 9 +++++++++ src/library/tactic/expr_to_tactic.h | 2 ++ 2 files changed, 11 insertions(+) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index dc84df73a..e3672a24a 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -429,7 +429,16 @@ struct info_manager::imp { m_line_data[l].insert(mk_symbol_info(c, s)); } + static bool is_tactic_id(name const & id) { + if (id.is_atomic()) + return id == get_tactic_name(); + else + return is_tactic_id(id.get_prefix()); + } + void add_identifier_info(unsigned l, unsigned c, name const & full_id) { + if (is_tactic_id(full_id)) + return; lock_guard lc(m_mutex); if (m_block_new_info) return; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index d596ebcf8..8672ed213 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -27,6 +27,8 @@ bool has_tactic_decls(environment const & env); */ tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p); +name const & get_tactic_name(); + expr const & get_tactic_expr_type(); expr mk_tactic_expr(expr const & e); bool is_tactic_expr(expr const & e);