michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/server): add ECHO command for debugging purposes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-28 07:40:02 -07:00
parent 1a8eb9799e
commit 823a3a7c56
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/server.cpp
View file

@ -213,6 +213,7 @@ 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 std::string g_echo("ECHO");
static bool is_command(std::string const & cmd, std::string const & line) {
return line.compare(0, cmd.size(), cmd) == 0;
@ -356,6 +357,9 @@ bool server::operator()(std::istream & in) {
std::string fname = line.substr(g_visit.size());
trim(fname);
visit_file(fname);
} else if (is_command(g_echo, line)) {
std::string str = line.substr(g_echo.size());
m_out << "--" << str << "\n";
} else if (is_command(g_replace, line)) {
unsigned linenum = get_linenum(line, g_replace);
read_line(in, line);