feat(*): make sections 'permanent', and add 'transient' contexts, closes #88

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/emacs/lean-mode.el

@@ -64,7 +64,7 @@
 (define-generic-mode
     'lean-mode     ;; name of the mode to create
   '("--")          ;; comments start with
-  '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "private" "using" "namespace" "builtin" "including" "instance" "section" "set_option" "add_rewrite" "extends") ;; some keywords
+  '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "private" "using" "namespace" "builtin" "including" "instance" "section" "context" "set_option" "add_rewrite" "extends") ;; some keywords
   '(("\\_<\\(bool\\|int\\|nat\\|real\\|Prop\\|Type\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)

src/frontends/lean/builtin_cmds.cpp

@@ -67,7 +67,15 @@ environment section_cmd(parser & p) {
     if (p.curr_is_identifier())
         n = p.check_atomic_id_next("invalid section, atomic identifier expected");
     p.push_local_scope();
-    return push_scope(p.env(), p.ios(), true, n);
+    return push_scope(p.env(), p.ios(), scope_kind::Section, n);
+}
+
+environment context_cmd(parser & p) {
+    name n;
+    if (p.curr_is_identifier())
+        n = p.check_atomic_id_next("invalid context, atomic identifier expected");
+    p.push_local_scope();
+    return push_scope(p.env(), p.ios(), scope_kind::Context, n);
 }
 
 environment namespace_cmd(parser & p) {
@@ -75,11 +83,11 @@ environment namespace_cmd(parser & p) {
     name n = p.check_atomic_id_next("invalid namespace declaration, atomic identifier expected");
     if (is_root_namespace(n))
         throw parser_error(sstream() << "invalid namespace name, '" << n << "' is reserved", pos);
-    return push_scope(p.env(), p.ios(), false, n);
+    return push_scope(p.env(), p.ios(), scope_kind::Namespace, n);
 }
 
 environment end_scoped_cmd(parser & p) {
-    if (in_section(p.env()))
+    if (in_section_or_context(p.env()))
         p.pop_local_scope();
     if (p.curr_is_identifier()) {
         name n = p.check_atomic_id_next("invalid end of scope, atomic identifier expected");
@@ -300,6 +308,7 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("exit",         "exit", exit_cmd));
     add_cmd(r, cmd_info("print",        "print a string", print_cmd));
     add_cmd(r, cmd_info("section",      "open a new section", section_cmd));
+    add_cmd(r, cmd_info("context",      "open a new context", context_cmd));
     add_cmd(r, cmd_info("namespace",    "open a new namespace", namespace_cmd));
     add_cmd(r, cmd_info("end",          "close the current namespace/section", end_scoped_cmd));
     add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));

src/frontends/lean/decl_cmds.cpp

@@ -33,7 +33,7 @@ environment universe_cmd(parser & p) {
     name n = p.check_id_next("invalid universe declaration, identifier expected");
     check_atomic(n);
     environment env = p.env();
-    if (in_section(env)) {
+    if (in_section_or_context(env)) {
         p.add_local_level(n, mk_param_univ(n));
     } else {
         name const & ns = get_namespace(env);
@@ -79,7 +79,7 @@ static environment declare_var(parser & p, environment env,
                                bool is_axiom, optional<binder_info> const & _bi, pos_info const & pos) {
     binder_info bi;
     if (_bi) bi = *_bi;
-    if (in_section(p.env())) {
+    if (in_section_or_context(p.env())) {
         p.add_local(p.save_pos(mk_local(n, type, bi), pos));
         return env;
     } else {
@@ -100,7 +100,7 @@ static environment declare_var(parser & p, environment env,
 
 /** \brief If we are in a section, then add the new local levels to it. */
 static void update_section_local_levels(parser & p, level_param_names const & new_ls) {
-    if (in_section(p.env())) {
+    if (in_section_or_context(p.env())) {
         for (auto const & l : new_ls)
             p.add_local_level(l, mk_param_univ(l));
     }
@@ -109,7 +109,7 @@ static void update_section_local_levels(parser & p, level_param_names const & ne
 optional<binder_info> parse_binder_info(parser & p) {
     optional<binder_info> bi = p.parse_optional_binder_info();
     if (bi)
-        check_in_section(p);
+        check_in_section_or_context(p);
     return bi;
 }
 
@@ -119,10 +119,10 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
     name n = p.check_id_next("invalid declaration, identifier expected");
     check_atomic(n);
     buffer<name> ls_buffer;
-    if (p.curr_is_token(g_llevel_curly) && in_section(p.env()))
+    if (p.curr_is_token(g_llevel_curly) && in_section_or_context(p.env()))
         throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
     optional<parser::local_scope> scope1;
-    if (!in_section(p.env()))
+    if (!in_section_or_context(p.env()))
         scope1.emplace(p);
     parse_univ_params(p, ls_buffer);
     expr type;
@@ -138,7 +138,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
     }
     p.parse_close_binder_info(bi);
     level_param_names ls;
-    if (in_section(p.env())) {
+    if (in_section_or_context(p.env())) {
         ls = to_level_param_names(collect_univ_params(type));
     } else {
         update_univ_parameters(ls_buffer, collect_univ_params(type), p);
@@ -274,7 +274,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         real_n     = ns + n;
     }
 
-    if (in_section(env)) {
+    if (in_section_or_context(env)) {
         buffer<expr> section_ps;
         collect_section_locals(type, value, p, section_ps);
         type = Pi_as_is(section_ps, type, p);
@@ -364,7 +364,7 @@ static environment variables_cmd(parser & p) {
         }
         p.next();
         optional<parser::local_scope> scope1;
-        if (!in_section(p.env()))
+        if (!in_section_or_context(p.env()))
             scope1.emplace(p);
         expr type = p.parse_expr();
         p.parse_close_binder_info(bi);

src/frontends/lean/inductive_cmd.cpp

@@ -329,7 +329,7 @@ struct inductive_cmd_fn {
 
     /** \brief Include in m_levels any section level referenced by decls. */
     void include_section_levels(buffer<inductive_decl> const & decls) {
-        if (!in_section(m_env))
+        if (!in_section_or_context(m_env))
             return;
         name_set all_lvl_params;
         for (auto const & d : decls) {
@@ -382,7 +382,7 @@ struct inductive_cmd_fn {
         The section parameters are stored in section_params
     */
     void abstract_section_locals(buffer<inductive_decl> & decls, buffer<expr> & section_params) {
-        if (!in_section(m_env))
+        if (!in_section_or_context(m_env))
             return;
         expr_struct_set section_locals;
         collect_section_locals(decls, section_locals);
@@ -508,7 +508,7 @@ struct inductive_cmd_fn {
     /** \brief Create an alias for the fully qualified name \c full_id. */
     environment create_alias(environment env, name const & full_id, levels const & section_leves, buffer<expr> const & section_params) {
         name id(full_id.get_string());
-        if (in_section(env)) {
+        if (in_section_or_context(env)) {
             expr r = mk_explicit(mk_constant(full_id, section_leves));
             r = mk_app(r, section_params);
             m_p.add_local_expr(id, r);

src/frontends/lean/parser.cpp

@@ -999,7 +999,7 @@ name parser::check_constant_next(char const * msg) {
     name id = check_id_next(msg);
     expr e  = id_to_expr(id, p);
 
-    if (in_section(m_env) && is_implicit(e)) {
+    if (in_section_or_context(m_env) && is_implicit(e)) {
         e = get_app_fn(get_implicit_arg(e));
         if (is_explicit(e))
             e = get_explicit_arg(e);

src/frontends/lean/parser.h

@@ -159,6 +159,7 @@ class parser {
     bool parse_local_notation_decl(buffer<notation_entry> * entries);
 
     friend environment section_cmd(parser & p);
+    friend environment context_cmd(parser & p);
     friend environment end_scoped_cmd(parser & p);
 
     void push_local_scope();

src/frontends/lean/parser_config.cpp

@@ -54,8 +54,8 @@ struct token_config {
     }
 };
 
-template class scoped_ext<token_config>;
+template class scoped_ext<token_config, true>;
-typedef scoped_ext<token_config> token_ext;
+typedef scoped_ext<token_config, true> token_ext;
 
 environment add_token(environment const & env, token_entry const & e) {
     return token_ext::add_entry(env, get_dummy_ios(), e);
@@ -188,8 +188,8 @@ struct notation_config {
     }
 };
 
-template class scoped_ext<notation_config>;
+template class scoped_ext<notation_config, true>;
-typedef scoped_ext<notation_config> notation_ext;
+typedef scoped_ext<notation_config, true> notation_ext;
 
 environment add_notation(environment const & env, notation_entry const & e) {
     return notation_ext::add_entry(env, get_dummy_ios(), e);

src/frontends/lean/structure_cmd.cpp

@@ -118,7 +118,7 @@ struct structure_cmd_fn {
 
     /** \brief Include in m_level_names any section level referenced m_type and m_fields */
     void include_section_levels() {
-        if (!in_section(m_env))
+        if (!in_section_or_context(m_env))
             return;
         name_set all_lvl_params;
         all_lvl_params = collect_univ_params(m_type);
@@ -150,7 +150,7 @@ struct structure_cmd_fn {
         The section parameters are stored in section_params
     */
     void abstract_section_locals(buffer<expr> & section_params) {
-        if (!in_section(m_env))
+        if (!in_section_or_context(m_env))
             return;
         expr_struct_set section_locals;
         collect_section_locals(section_locals);

src/frontends/lean/token_table.cpp

@@ -77,7 +77,7 @@ token_table init_token_table() {
                                "variables", "[private]", "[inline]", "[fact]", "[instance]", "[module]", "[coercion]",
                                "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
-                               "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
+                               "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
                                "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
                                "add_begin_end_tactic", "set_begin_end_tactic", "instance", "#erase_cache", nullptr};
 

src/frontends/lean/util.cpp

@@ -19,8 +19,8 @@ void check_atomic(name const & n) {
         throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
 }
 
-void check_in_section(parser const & p) {
+void check_in_section_or_context(parser const & p) {
-    if (!in_section(p.env()))
+    if (!in_section_or_context(p.env()))
         throw exception(sstream() << "invalid command, it must be used in a section");
 }
 static name g_root("_root_");

src/frontends/lean/util.h

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 void check_atomic(name const & n);
-void check_in_section(parser const & p);
+void check_in_section_or_context(parser const & p);
 bool is_root_namespace(name const & n);
 name remove_root_prefix(name const & n);
 /** \brief Return the levels in \c ls that are defined in the section. */

src/library/aliases.cpp

@@ -24,12 +24,12 @@ static environment update(environment const & env, aliases_ext const & ext);
 
 struct aliases_ext : public environment_extension {
     struct state {
-        bool                                      m_in_section;
+        bool                                      m_in_section_or_context;
         rb_map<name, list<name>, name_quick_cmp>  m_aliases;
         rb_map<name, name,       name_quick_cmp>  m_inv_aliases;
         rb_map<name, name,       name_quick_cmp>  m_level_aliases;
         rb_map<name, name,       name_quick_cmp>  m_inv_level_aliases;
-        state():m_in_section(false) {}
+        state():m_in_section_or_context(false) {}
 
         void add_expr_alias(name const & a, name const & e) {
             auto it = m_aliases.find(a);
@@ -62,7 +62,7 @@ struct aliases_ext : public environment_extension {
         } else {
             state s = head(scopes);
             s.add_expr_alias(a, e);
-            if (s.m_in_section) {
+            if (s.m_in_section_or_context) {
                 return cons(s, add_expr_alias_rec_core(tail(scopes), a, e));
             } else {
                 return cons(s, tail(scopes));
@@ -71,16 +71,16 @@ struct aliases_ext : public environment_extension {
     }
 
     void add_expr_alias_rec(name const & a, name const & e) {
-        if (m_state.m_in_section) {
+        if (m_state.m_in_section_or_context) {
             m_scopes = add_expr_alias_rec_core(m_scopes, a, e);
         } else {
             add_expr_alias(a, e);
         }
     }
 
-    void push(bool in_section) {
+    void push(bool in_section_or_context) {
         m_scopes = cons(m_state, m_scopes);
-        m_state.m_in_section = in_section;
+        m_state.m_in_section_or_context = in_section_or_context;
     }
 
     void pop() {
@@ -93,16 +93,16 @@ struct aliases_ext : public environment_extension {
         return env;
     }
 
-    static environment push_scope(environment const & env, bool in_section) {
+    static environment push_scope(environment const & env, scope_kind k) {
         aliases_ext ext = get_extension(env);
-        ext.push(in_section);
+        ext.push(k != scope_kind::Namespace);
         environment new_env = update(env, ext);
-        if (!::lean::in_section(new_env))
+        if (!::lean::in_section_or_context(new_env))
             new_env = add_aliases(new_env, get_namespace(new_env), name());
         return new_env;
     }
 
-    static environment pop_scope(environment const & env, bool) {
+    static environment pop_scope(environment const & env, scope_kind) {
         aliases_ext ext = get_extension(env);
         ext.pop();
         return update(env, ext);

src/library/scoped_ext.cpp

@@ -27,10 +27,10 @@ void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn p
 }
 
 struct scope_mng_ext : public environment_extension {
-    name_set     m_namespace_set; // all namespaces registered in the system
+    name_set         m_namespace_set; // all namespaces registered in the system
-    list<name>   m_namespaces;    // stack of namespaces/sections
+    list<name>       m_namespaces;    // stack of namespaces/sections
-    list<name>   m_headers;       // namespace/section header
+    list<name>       m_headers;       // namespace/section header
-    list<bool>   m_in_section;
+    list<scope_kind> m_scope_kinds;
 };
 
 struct scope_mng_ext_reg {
@@ -55,9 +55,14 @@ list<name> const & get_namespaces(environment const & env) {
     return get_extension(env).m_namespaces;
 }
 
-bool in_section(environment const & env) {
+bool in_section_or_context(environment const & env) {
     scope_mng_ext const & ext = get_extension(env);
-    return !is_nil(ext.m_in_section) && head(ext.m_in_section);
+    return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) != scope_kind::Namespace;
+}
+
+bool in_context(environment const & env) {
+    scope_mng_ext const & ext = get_extension(env);
+    return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) == scope_kind::Context;
 }
 
 environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c) {
@@ -82,9 +87,9 @@ optional<name> to_valid_namespace_name(environment const & env, name const & n)
 }
 
 static std::string g_new_namespace_key("nspace");
-environment push_scope(environment const & env, io_state const & ios, bool add_sec, name const & n) {
+environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
-    if (!add_sec && in_section(env))
+    if (k == scope_kind::Namespace && in_section_or_context(env))
-        throw exception("invalid namespace declaration, a namespace cannot be declared inside a section");
+        throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");
     name new_n = get_namespace(env) + n;
     scope_mng_ext ext = get_extension(env);
     bool save_ns = false;
@@ -92,14 +97,14 @@ environment push_scope(environment const & env, io_state const & ios, bool add_s
         save_ns  = true;
         ext.m_namespace_set.insert(new_n);
     }
-    ext.m_namespaces = cons(new_n, ext.m_namespaces);
+    ext.m_namespaces  = cons(new_n, ext.m_namespaces);
-    ext.m_headers    = cons(n, ext.m_headers);
+    ext.m_headers     = cons(n, ext.m_headers);
-    ext.m_in_section = cons(add_sec, ext.m_in_section);
+    ext.m_scope_kinds = cons(k, ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<2>(t)(r, add_sec);
+        r = std::get<2>(t)(r, k);
     }
-    if (!add_sec)
+    if (k == scope_kind::Namespace)
         r = using_namespace(r, ios, n);
     if (save_ns)
         r = module::add(r, g_new_namespace_key, [=](serializer & s) { s << new_n; });
@@ -122,16 +127,16 @@ register_module_object_reader_fn g_namespace_reader(g_new_namespace_key, namespa
 environment pop_scope(environment const & env, name const & n) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
-        throw exception("invalid end of scope, there are no open namespaces/sections");
+        throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
     if (n != head(ext.m_headers))
         throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '" << head(ext.m_headers) << "', and ends with '" << n << "'");
-    bool in_section  = head(ext.m_in_section);
+    scope_kind k      = head(ext.m_scope_kinds);
-    ext.m_namespaces = tail(ext.m_namespaces);
+    ext.m_namespaces  = tail(ext.m_namespaces);
-    ext.m_headers    = tail(ext.m_headers);
+    ext.m_headers     = tail(ext.m_headers);
-    ext.m_in_section = tail(ext.m_in_section);
+    ext.m_scope_kinds = tail(ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<3>(t)(r, in_section);
+        r = std::get<3>(t)(r, k);
     }
     return r;
 }
@@ -156,13 +161,14 @@ static int using_namespace_objects(lua_State * L) {
 static int push_scope(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 1)
-        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), true));
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Context));
     else if (nargs == 2)
-        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), false, to_name_ext(L, 2)));
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Namespace, to_name_ext(L, 2)));
-    else if (nargs == 3)
+    scope_kind k = static_cast<scope_kind>(lua_tonumber(L, 3));
-        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), lua_toboolean(L, 3), to_name_ext(L, 2)));
+    if (nargs == 3)
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), k, to_name_ext(L, 2)));
     else
-        return push_environment(L, push_scope(to_environment(L, 1), to_io_state(L, 4), lua_toboolean(L, 3), to_name_ext(L, 2)));
+        return push_environment(L, push_scope(to_environment(L, 1), to_io_state(L, 4), k, to_name_ext(L, 2)));
 }
 
 static int pop_scope(lua_State * L) {
@@ -177,5 +183,11 @@ void open_scoped_ext(lua_State * L) {
     SET_GLOBAL_FUN(using_namespace_objects, "using_namespace_objects");
     SET_GLOBAL_FUN(push_scope, "push_scope");
     SET_GLOBAL_FUN(pop_scope, "pop_scope");
+
+    lua_newtable(L);
+    SET_ENUM("Namespace",   scope_kind::Namespace);
+    SET_ENUM("Section",     scope_kind::Section);
+    SET_ENUM("Context",     scope_kind::Context);
+    lua_setglobal(L, "scope_kind");
 }
 }

src/library/scoped_ext.h

@@ -15,22 +15,24 @@ Author: Leonardo de Moura
 #include "library/module.h"
 
 namespace lean {
+enum class scope_kind { Namespace, Section, Context };
 typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
-typedef environment (*push_scope_fn)(environment const &, bool);
+typedef environment (*push_scope_fn)(environment const &, scope_kind);
-typedef environment (*pop_scope_fn)(environment const &, bool);
+typedef environment (*pop_scope_fn)(environment const &, scope_kind);
 
 void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop);
 /** \brief Use objects defined in the namespace \c n, if \c c is not the anonymous name, then only object from "class" \c c are considered. */
 environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c = name());
 /** \brief Create a new scope, all scoped extensions are notified. */
-environment push_scope(environment const & env, io_state const & ios, bool section, name const & n = name());
+environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n = name());
 /** \brief Delete the most recent scope, all scoped extensions are notified. */
 environment pop_scope(environment const & env, name const & n = name());
 bool has_open_scopes(environment const & env);
 
 name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);
-bool in_section(environment const & env);
+bool in_section_or_context(environment const & env);
+bool in_context(environment const & env);
 
 /** \brief Check if \c n may be a reference to a namespace, if it is return it.
     The procedure checks if \c n is a registered namespace, if it is not, it tries
@@ -49,7 +51,7 @@ void open_scoped_ext(lua_State * L);
    \brief Auxilary template used to simplify the creation of environment extensions that support
    the scope
 */
-template<typename Config>
+template<typename Config, bool TransientSection = false>
 class scoped_ext : public environment_extension {
     typedef typename Config::state            state;
     typedef typename Config::entry            entry;
@@ -150,17 +152,23 @@ public:
     static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) {
         return update(env, get(env).using_namespace(env, ios, n));
     }
-    static environment push_fn(environment const & env, bool) {
+    static environment push_fn(environment const & env, scope_kind k) {
-        return update(env, get(env).push());
+        if (k != scope_kind::Section || TransientSection)
+            return update(env, get(env).push());
+        else
+            return env;
     }
-    static environment pop_fn(environment const & env, bool) {
+    static environment pop_fn(environment const & env, scope_kind k) {
-        return update(env, get(env).pop());
+        if (k != scope_kind::Section || TransientSection)
+            return update(env, get(env).pop());
+        else
+            return env;
     }
     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) {
-        if (in_section(env)) {
+        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);
@@ -189,6 +197,6 @@ public:
     }
 };
 
-template<typename Config>
+template<typename Config, bool TransientSection>
-typename scoped_ext<Config>::reg scoped_ext<Config>::g_ext;
+typename scoped_ext<Config, TransientSection>::reg scoped_ext<Config, TransientSection>::g_ext;
 }

tests/lean/t14.lean

@@ -1,4 +1,3 @@
-
 namespace foo
   variable A : Type.{1}
   variable a : A
@@ -6,25 +5,25 @@ namespace foo
   variable c : A
 end foo
 
-section
+context
   using foo (renaming a->b x->y) (hiding c)
   check b
   check y
   check c -- Error
 end
 
-section
+context
   using foo (a x)
   check a
   check x
   check c -- Error
 end
 
-section
+context
   using foo (a x) (hiding c) -- Error
 end
 
-section
+context
   using foo
   check a
   check c
@@ -36,18 +35,18 @@ namespace foo
   infix `*`:75 := f
 end foo
 
-section
+context
   using foo
   check a * c
 end
 
-section
+context
   using [notation] foo -- use only the notation
   check foo.a * foo.c
   check a * c -- Error
 end
 
-section
+context
   using [decls] foo -- use only the declarations
   check f a c
   check a*c -- Error

tests/lean/t14.lean.expected.out

@@ -1,15 +1,15 @@
 b : A
 y : A
-t14.lean:13:8: error: unknown identifier 'c'
+t14.lean:12:8: error: unknown identifier 'c'
 a : foo.A
 x : foo.A
-t14.lean:20:8: error: unknown identifier 'c'
+t14.lean:19:8: error: unknown identifier 'c'
-t14.lean:24:27: error: invalid 'using' command option, mixing explicit and implicit 'using' options
+t14.lean:23:27: error: invalid 'using' command option, mixing explicit and implicit 'using' options
 a : A
 c : A
 A : Type
 f a c : A
 foo.f foo.a foo.c : foo.A
-t14.lean:47:8: error: unknown identifier 'a'
+t14.lean:46:8: error: unknown identifier 'a'
 f a c : A
-t14.lean:53:9: error: unexpected token
+t14.lean:52:9: error: unexpected token

tests/lean/t3.lean.expected.out

@@ -5,7 +5,7 @@ Type
 t3.lean:9:16: error: unknown universe 'v'
 Type
 t3.lean:14:16: error: unknown universe 'z'
-t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section
+t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section or context
 Type
 Type
 Type