From d402b2a467bad90e4032d5d28209da3e0020083f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 17 Feb 2017 15:17:56 +0100
Subject: [PATCH] feat(frontends/lean/print_cmd): add to info_manager when not
 overloaded

---
 src/frontends/lean/print_cmd.cpp              | 10 ++++++++++
 tests/lean/interactive/info.lean              |  3 +++
 tests/lean/interactive/info.lean.expected.out |  2 ++
 3 files changed, 15 insertions(+)

diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index f8184f9390..0266269162 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/info_manager.h"
 
 // TODO(gabriel): make print command async
 
@@ -386,6 +387,15 @@ bool print_id_info(parser & p, message_builder & out, name const & id, bool show
         }
         // print_patterns(p, c);
     }
+
+    // add to info_manager when not overloaded
+    if (auto c = head_opt(cs))
+        if (!tail(cs))
+            if (auto infom = get_global_info_manager()) {
+                infom->add_identifier_info(pos.first, pos.second, *c);
+                infom->add_type_info(pos.first, pos.second, p.env().get(*c).get_type());
+            }
+
     if (found) return true;
 
     // variables and parameters
diff --git a/tests/lean/interactive/info.lean b/tests/lean/interactive/info.lean
index c7152198b4..265e146a97 100644
--- a/tests/lean/interactive/info.lean
+++ b/tests/lean/interactive/info.lean
@@ -14,3 +14,6 @@ example := [tt]
 
 example := [tt]++[]
              --^ "command": "info"
+
+print id
+     --^ "command": "info"
diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out
index 0a8edac7f6..07918bffd6 100644
--- a/tests/lean/interactive/info.lean.expected.out
+++ b/tests/lean/interactive/info.lean.expected.out
@@ -1,3 +1,4 @@
+{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[reducible]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"},"response":"additional_message"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"source":},"response":"ok","seq_num":2}
 {"record":{"doc":"reducible"},"response":"ok","seq_num":5}
@@ -5,3 +6,4 @@
 {"record":{"doc":"(trace) enable/disable tracing for the given module and submodules"},"response":"ok","seq_num":10}
 {"record":{"full-id":"list.cons","source":,"type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":13}
 {"record":{"full-id":"append","source":,"type":"Π {α : Type} [_inst_1 : has_append α], α → α → α"},"response":"ok","seq_num":16}
+{"record":{"full-id":"id","source":,"type":"Π {α : Sort u}, α → α"},"response":"ok","seq_num":19}