From 4eb2690c32aa23e91f78c241bc74110458e97ce2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Jan 2016 13:35:08 -0800
Subject: [PATCH] feat(library/scoped_ext): store set of opened namespaces

---
 src/frontends/lean/builtin_cmds.cpp |  1 +
 src/library/scoped_ext.cpp          | 17 ++++++++++++++---
 src/library/scoped_ext.h            |  5 +++++
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 41cfe42de9..ab9c005737 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/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())) {
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index f73c9014f4..1eb42a21b1 100644
--- a/src/library/scoped_ext.cpp
+++ b/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()) {
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index d68efa8e06..a822f71546 100644
--- a/src/library/scoped_ext.h
+++ b/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