fix(frontends/lean/info_manager): disable notation pretty printer when displaying OVERLOAD
information
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
This commit is contained in:
parent
92acd9affc
commit
2f62a5e887
1 changed files with 1 additions and 0 deletions
|
@ -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) {
|
||||
|
|
Loading…
Reference in a new issue