Skip to content

Commit

Permalink
fix(frontends/lean/info_manager): fix widget updates in by ... (#312)
Browse files Browse the repository at this point in the history
  • Loading branch information
gebner committed Jun 10, 2020
1 parent 6d32859 commit 485d7ad
Showing 1 changed file with 6 additions and 2 deletions.
8 changes: 6 additions & 2 deletions src/frontends/lean/info_manager.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -327,8 +327,12 @@ bool info_manager::update_widget(pos_info pos, json & record, json const & messa
// get last widget_info (only the last widget is shown if there is more than one at a position)
widget_info * w = nullptr;
for (auto & d : *ds) {
if (auto cw = is_widget_info(d))
w = const_cast<widget_info *>(cw);
if (auto cw = is_widget_info(d)) {
// HACK(gabriel): if there are any non-term goals, pick the last non-term goal
// these are also prioritized in the info request....
if (!w || dynamic_cast<term_goal_data *>(w) || !is_term_goal(d))
w = const_cast<widget_info *>(cw);
}
}
if (w) {
w->update(message, record);
Expand Down

0 comments on commit 485d7ad

Please sign in to comment.