From cbafa0dbf9c0a3b94a546867a9ad44c9c8f3a3d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Sep 2014 12:14:00 -0700 Subject: [PATCH] feat(library/scoped_ext): allow extensions to mark whether an entry is persistent or not --- src/library/scoped_ext.h | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index bc6022758..bdec71616 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -189,15 +189,17 @@ public: static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) { return update(env, get(env)._register_entry(env, ios, n, e)); } - static environment add_entry(environment env, io_state const & ios, entry const & e) { + static environment add_entry(environment env, io_state const & ios, entry const & e, bool persistent = true) { if ((!TransientSection && in_context(env)) || (TransientSection && in_section_or_context(env))) { return update(env, get(env)._add_tmp_entry(env, ios, e)); } else { name n = get_namespace(env); - env = module::add(env, get_serialization_key(), [=](serializer & s) { - s << n; - write_entry(s, e); - }); + if (persistent) { + env = module::add(env, get_serialization_key(), [=](serializer & s) { + s << n; + write_entry(s, e); + }); + } return update(env, get(env)._add_entry(env, ios, e)); } }