From a97d7ffed7ee843a8459d4808762e67822586c50 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Nov 2014 13:31:42 -0800
Subject: [PATCH] feat(frontends/lean/builtin_cmds): display 'print' command
 output as flycheck information

---
 src/frontends/lean/builtin_cmds.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 865f678b3..1993ac913 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -107,6 +107,11 @@ static void print_fields(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) {
         p.regular_stream() << p.get_str_val() << endl;
         p.next();