From 22ae42d3af1cfaca5263b743f32e4826ee333a94 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Oct 2014 14:29:17 -0700 Subject: [PATCH] fix(frontends/lean/info_manager): use fresh formatter displaying each info object The formatter may cache results. --- src/frontends/lean/info_manager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 422a100b3..ea970df4c 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -564,8 +564,8 @@ struct info_manager::imp { void display_core(environment const & env, options const & o, io_state const & ios, unsigned line, optional const & col) { - io_state_stream out = regular(env, ios).update_options(o); m_line_data[line].for_each([&](info_data const & d) { + io_state_stream out = regular(env, ios).update_options(o); if ((!col && d.is_cheap()) || (col && d.get_column() == *col)) d.display(out, line); });