From 366bf70ccd6aca68c43f3fc797e1caad7ae68ef0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 21:20:25 -0800 Subject: [PATCH] fix(frontends/lean/elaborator): do not display flycheck related messages when --flycheck is not on --- src/frontends/lean/elaborator.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4a82ba9de..ac1d702db 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1053,8 +1053,10 @@ void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr if (auto p = pip()->get_pos_info(ptac)) { auto out = regular(env(), ios()); flycheck_information info(out); - display_information_pos(out, pip()->get_file_name(), p->first, p->second); - out << " proof state:\n" << ps.pp(env(), ios()) << "\n"; + if (info.enabled()) { + display_information_pos(out, pip()->get_file_name(), p->first, p->second); + out << " proof state:\n" << ps.pp(env(), ios()) << "\n"; + } } } ps = r->first;