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

feat(frontends/lean/builtin_cmds): display 'print' command output as flycheck information

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-29 13:31:42 -08:00
parent 6fbbf66565
commit a97d7ffed7
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/builtin_cmds.cpp
View file

@ -107,6 +107,11 @@ static void print_fields(parser & p) {
} }
environment print_cmd(parser & p) { environment print_cmd(parser & p) {
flycheck_information info(p.regular_stream());
if (info.enabled()) {
p.display_information_pos(p.cmd_pos());
p.regular_stream() << "print result:\n";
}
if (p.curr() == scanner::token_kind::String) { if (p.curr() == scanner::token_kind::String) {
p.regular_stream() << p.get_str_val() << endl; p.regular_stream() << p.get_str_val() << endl;
p.next(); p.next();