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

fix(frontends/lean/info_manager): only store holes once

Browse source
This commit is contained in:
Gabriel Ebner 2017-06-15 10:22:48 +02:00
parent bce1f10ae4
commit b09fee680c
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<pos_info> 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)));

1
src/frontends/lean/info_manager.cpp
View file

@ -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) {