michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/scoped_ext): allow extensions to mark whether an entry is

Browse source 
persistent or not
This commit is contained in:
Leonardo de Moura 2014-09-19 12:14:00 -07:00
parent 5b9b814fd1
commit cbafa0dbf9
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/scoped_ext.h
View file

@ -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));
}
}