From dc92f67588ebe7f4122b90f1edcbfe5aa419f9ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Oct 2014 08:42:20 -0700 Subject: [PATCH] feat(frontends/lean/server): CLEAR_CACHE forces buffer to be reprocessed --- src/frontends/lean/server.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 9880d1356..9eaca1d02 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -872,7 +872,10 @@ bool server::operator()(std::istream & in) { read_line(in, line); eval(line); } else if (is_command(*g_clear_cache, line)) { + interrupt_worker(); m_cache.clear(); + if (m_file) + process_from(0); } else if (is_command(*g_options, line)) { show_options(); } else if (is_command(*g_wait, line)) {