From fab4eb0d69ee3079e27dfb5706ca4e37ccbdf657 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Aug 2014 10:31:01 -0700
Subject: [PATCH] feat(frontends/lean/server): add CLEAR_CACHE command, closes
 #100

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/server.cpp    | 3 +++
 src/library/definition_cache.cpp | 5 +++++
 src/library/definition_cache.h   | 2 ++
 3 files changed, 10 insertions(+)

diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index d2b8a3478d..c71dd93771 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -97,6 +97,7 @@ static std::string g_info("INFO");
 static std::string g_set("SET");
 static std::string g_eval("EVAL");
 static std::string g_wait("WAIT");
+static std::string g_clear_cache("CLEAR_CACHE");
 
 static bool is_command(std::string const & cmd, std::string const & line) {
     return line.compare(0, cmd.size(), cmd) == 0;
@@ -319,6 +320,8 @@ bool server::operator()(std::istream & in) {
             } else if (is_command(g_eval, line)) {
                 read_line(in, line);
                 eval(line);
+            } else if (is_command(g_clear_cache, line)) {
+                m_cache.clear();
             } else if (is_command(g_wait, line)) {
                 if (m_thread_ptr) {
                     m_thread_ptr->join();
diff --git a/src/library/definition_cache.cpp b/src/library/definition_cache.cpp
index 3243292310..02ff030023 100644
--- a/src/library/definition_cache.cpp
+++ b/src/library/definition_cache.cpp
@@ -150,6 +150,11 @@ void definition_cache::erase(name const & n) {
     m_definitions.erase(n);
 }
 
+void definition_cache::clear() {
+    lock_guard<mutex> lc(m_mutex);
+    m_definitions.clear();
+}
+
 optional<std::tuple<level_param_names, expr, expr>> definition_cache::find(name const & n, expr const & pre_type, expr const & pre_value) {
     entry const * it;
     {
diff --git a/src/library/definition_cache.h b/src/library/definition_cache.h
index 83e568f24c..1c1c5a500d 100644
--- a/src/library/definition_cache.h
+++ b/src/library/definition_cache.h
@@ -36,5 +36,7 @@ public:
     void load(std::istream & in);
     /** \brief Remove the entry named \c n from the cache. */
     void erase(name const & n);
+    /** \brief Clear the whole cache */
+    void clear();
 };
 }