feat(library/scoped_ext): store set of opened namespaces

src/frontends/lean/builtin_cmds.cpp

@@ -327,6 +327,7 @@ environment open_export_cmd(parser & p, bool open) {
             env = export_namespace(env, p.ios(), ns, metacls);
         if (decls) {
             // Remark: we currently to not allow renaming and hiding of universe levels
+            env = mark_namespace_as_open(env, ns);
             buffer<name> exceptions;
             bool found_explicit = false;
             while (p.curr_is_token(get_lparen_tk())) {

src/library/scoped_ext.cpp

@@ -22,9 +22,10 @@ void register_scoped_ext(name const & c, using_namespace_fn use, export_namespac
 }
 
 struct scope_mng_ext : public environment_extension {
-    name_set         m_namespace_set; // all namespaces registered in the system
-    list<name>       m_namespaces;    // stack of namespaces/sections
-    list<name>       m_headers;       // namespace/section header
+    name_set         m_namespace_set;     // all namespaces registered in the system
+    name_set         m_opened_namespaces; // set of namespaces marked as "open"
+    list<name>       m_namespaces;        // stack of namespaces/sections
+    list<name>       m_headers;           // namespace/section header
     list<scope_kind> m_scope_kinds;
 };
 
@@ -71,6 +72,16 @@ bool is_metaclass(name const & n) {
     return false;
 }
 
+environment mark_namespace_as_open(environment const & env, name const & n) {
+    scope_mng_ext ext = get_extension(env);
+    ext.m_opened_namespaces.insert(n);
+    return update(env, ext);
+}
+
+name_set get_opened_namespaces(environment const & env) {
+    return get_extension(env).m_opened_namespaces;
+}
+
 environment using_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses) {
     environment r = env;
     for (auto const & t : get_exts()) {

src/library/scoped_ext.h

@@ -76,6 +76,11 @@ bool in_section(environment const & env);
     Then, the procedure tries n, 'foo.bla.boo'+n, 'foo.bla'+n, 'foo'+n. */
 optional<name> to_valid_namespace_name(environment const & env, name const & n);
 
+/** \brief Mark the given namespace as opened */
+environment mark_namespace_as_open(environment const & env, name const & n);
+/** \brief Return the set of namespaces marked as "open" using \c mark_namespace_as_open. */
+name_set get_opened_namespaces(environment const & env);
+
 void open_scoped_ext(lua_State * L);
 
 /** \brief Auxilary template used to simplify the creation of environment extensions that support