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

feat(frontends/lean/tactic_notation): fall back to tactic info when hovering over/between parameters

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-16 12:53:40 +01:00 • committed by Leonardo de Moura
parent 9b5e7ddcda
commit 24e7e87f7d
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/tactic_notation.cpp
View file

@ -239,7 +239,16 @@ struct parse_tactic_fn {
expr r;
auto pos = m_p.pos();
if (auto dname = is_auto_quote_tactic(m_p, m_tac_class)) {
r = parse_auto_quote_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error);
try {
r = parse_auto_quote_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error);
} catch (break_at_pos_exception & e) {
if (!m_p.get_complete() && e.m_token_info.m_context == break_at_pos_exception::token_context::none) {
e.m_token_info.m_pos = pos;
e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic;
e.m_token_info.m_tac_class = m_tac_class;
}
throw;
}
} else if (is_curr_exact_shortcut(m_p)) {
expr arg = parse_qexpr();
r = m_p.mk_app(m_p.save_pos(mk_constant(m_tac_class + name({"interactive", "exact"})), pos), arg, pos);