From 2f62a5e887534d11a65929e726aa4d46d8274f1f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 22:05:43 -0700 Subject: [PATCH] fix(frontends/lean/info_manager): disable notation pretty printer when displaying `OVERLOAD` information MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We need that otherwise the Lean emacs mode will display useless overload information such as: [+] int.add : ℤ → ℤ → ℤ overloaded with #1 + #0, #1 + #0 Note that this only became an issue after we implemented the new pretty printer --- src/frontends/lean/info_manager.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index e8c156bf0..7cf743054 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -195,6 +195,7 @@ public: ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; options os = ios.get_options(); os = os.update(get_pp_full_names_option_name(), true); + os = os.update(get_pp_notation_option_name(), false); auto new_ios = ios.update_options(os); bool first = true; for (expr const & e : m_alts) {