From b09fee680c59d0ac673cb8a3e4bdc8a20ef6d20c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 15 Jun 2017 10:22:48 +0200 Subject: [PATCH] fix(frontends/lean/info_manager): only store holes once --- src/frontends/lean/elaborator.cpp | 6 +++--- src/frontends/lean/info_manager.cpp | 1 - 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 953488f416..5db8be9207 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3390,14 +3390,14 @@ void elaborator::process_hole(expr const & mvar, expr const & hole) { + pp_indent(pp_fn, val)); } expr ty = m_ctx.instantiate_mvars(m_ctx.infer(mvar)); - if (get_global_info_manager()) { + if (m_uses_infom) { expr args; optional begin_pos, end_pos; std::tie(args, begin_pos, end_pos) = get_hole_info(hole); if (begin_pos && end_pos) { tactic_state s = elaborator::mk_tactic_state_for(val); - get_global_info_manager()->add_hole_info(*begin_pos, *end_pos, s, args); + m_info.add_hole_info(*begin_pos, *end_pos, s, args); /* The following command is a hack to make sure we see the hole's type in Emacs */ - get_global_info_manager()->add_identifier_info(*begin_pos, "[goal]"); + m_info.add_identifier_info(*begin_pos, "[goal]"); } } m_ctx.assign(mvar, copy_tag(hole, mk_sorry(ty))); diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index bfcb3a7cfb..fa9f0501c2 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -160,7 +160,6 @@ void info_manager::add_hole_info(pos_info const & begin_pos, pos_info const & en #endif info_data d = mk_hole_info(s, hole_args, begin_pos, end_pos); add_info(begin_pos, d); - add_info(end_pos, d); } void info_manager::add_vm_obj_format_info(pos_info pos, environment const & env, vm_obj const & thunk) {