From 41935906a8b5ab976ffe22cebcbd68d99b216b2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jan 2015 13:02:14 -0800 Subject: [PATCH] chore(frontends/lean): use update_if_undef --- src/frontends/lean/builtin_cmds.cpp | 4 ++-- src/frontends/lean/info_manager.cpp | 8 ++++---- src/library/tactic/class_instance_synth.cpp | 4 ++-- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 7fd0278a6..5a2bd33d2 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -127,7 +127,7 @@ static bool print_parse_table(parser & p, parse_table const & t, bool nud, buffe bool found = false; io_state ios = p.ios(); options os = ios.get_options(); - os = os.update(get_pp_full_names_option_name(), true); + os = os.update_if_undef(get_pp_full_names_option_name(), true); os = os.update(get_pp_notation_option_name(), false); ios.set_options(os); optional tt(get_token_table(p.env())); @@ -307,7 +307,7 @@ environment check_cmd(parser & p) { auto reg = p.regular_stream(); formatter fmt = reg.get_formatter(); options opts = p.ios().get_options(); - opts = opts.update(get_pp_metavar_args_name(), true); + opts = opts.update_if_undef(get_pp_metavar_args_name(), true); fmt = fmt.update_options(opts); unsigned indent = get_pp_indent(opts); format r = group(fmt(e) + space() + colon() + nest(indent, line() + fmt(type))); diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index fe99fd589..e8f6e5946 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -176,7 +176,7 @@ public: virtual void display(io_state_stream const & ios, unsigned line) const { ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; options os = ios.get_options(); - os = os.update(get_pp_full_names_option_name(), true); + os = os.update_if_undef(get_pp_full_names_option_name(), true); auto new_ios = ios.update_options(os); for (unsigned i = 0; i < get_num_choices(m_choices); i++) { if (i > 0) @@ -197,8 +197,8 @@ public: virtual void display(io_state_stream const & ios, unsigned line) const { 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); + os = os.update_if_undef(get_pp_full_names_option_name(), true); + os = os.update_if_undef(get_pp_notation_option_name(), false); auto new_ios = ios.update_options(os); bool first = true; for (expr const & e : m_alts) { @@ -221,7 +221,7 @@ public: virtual void display(io_state_stream const & ios, unsigned line) const { ios << "-- COERCION|" << line << "|" << get_column() << "\n"; options os = ios.get_options(); - os = os.update(get_pp_coercions_option_name(), true); + os = os.update_if_undef(get_pp_coercions_option_name(), true); ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl; ios << "-- ACK" << endl; } diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index ec7a5e6e1..6ce3f7aa7 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -101,8 +101,8 @@ struct class_instance_context { m_trace_instances = get_class_trace_instances(ios.get_options()); m_max_depth = get_class_instance_max_depth(ios.get_options()); options opts = m_ios.get_options(); - opts = opts.update(get_pp_purify_metavars_name(), false); - opts = opts.update(get_pp_implicit_name(), true); + opts = opts.update_if_undef(get_pp_purify_metavars_name(), false); + opts = opts.update_if_undef(get_pp_implicit_name(), true); m_ios.set_options(opts); }