diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el
index 97c2d8f3a9..0f38041c9e 100644
--- a/src/emacs/lean-info.el
+++ b/src/emacs/lean-info.el
@@ -45,15 +45,13 @@
 
 (defun lean-get-info-record-at-point (cont)
   "Get info-record at the current point"
-  ;; TODO(sullrich): finding the start position should go into the server
-  (let ((pos (lean-find-hname-beg)))
-    (lean-server-send-command
-     'info (list :file_name (buffer-file-name)
-                 :line (line-number-at-pos pos)
-                 :column (lean-line-offset pos))
-     (cl-function
-      (lambda (&key record)
-        (funcall cont record))))))
+  (lean-server-send-command
+   'info (list :file_name (buffer-file-name)
+               :line (line-number-at-pos)
+               :column (lean-line-offset))
+   (cl-function
+    (lambda (&key record)
+      (funcall cont record)))))
 
 (cl-defun lean-find-definition-cont (&key file line column)
   (when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack))
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index e0fdae0bb1..b24b2b397f 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -210,48 +210,19 @@ parser::parser(environment const & env, io_state const & ios,
 parser::~parser() {
 }
 
-void parser::scan() {
-    if (m_info_at) {
-        m_curr = m_scanner.scan(m_env);
-        pos_info p = pos();
-        if (p.first == m_info_at_line) {
-            if (curr_is_identifier()) {
-                name const & id = get_name_val();
-                if (p.second <= m_info_at_col && m_info_at_col < p.second + id.utf8_size()) {
-                    auto out = mk_message(INFORMATION);
-                    bool ok = true;
-                    try {
-                        bool show_value = false;
-                        ok = print_id_info(*this, out, id, show_value, p);
-                    } catch (exception &) {
-                        ok = false;
-                    }
-                    if (!ok)
-                        out << "unknown identifier '" << id << "'\n";
-                    out.report();
-                    m_info_at = false;
-                }
-            } else if (curr_is_keyword()) {
-                name const & tk = get_token_info().token();
-                if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
-                    auto out = mk_message(INFORMATION);
-                    try {
-                        print_token_info(*this, out, tk);
-                    } catch (exception &) {}
-                    out.report();
-                    m_info_at = false;
-                }
-            } else if (curr_is_command()) {
-                name const & tk = get_token_info().token();
-                if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
-                    (mk_message(INFORMATION) << "'" << tk << "' is a command").report();
-                    m_info_at = false;
-                }
-            }
-        }
-    } else {
-        m_curr = m_scanner.scan(m_env);
+bool parser::check_break_at_pos(pos_info const & p, name const & tk) {
+    if (m_break_at_pos && p.first == m_break_at_pos->first && p.second <= m_break_at_pos->second) {
+        std::string s = tk.to_string();
+        if (utf8_char_pos(s.c_str(), m_break_at_pos->second - p.second))
+            return true;
     }
+    return false;
+}
+
+void parser::scan() {
+    if (curr_is_identifier() && check_break_at_pos(pos(), get_name_val()))
+        throw break_at_pos_exception(pos(), get_name_val());
+    m_curr = m_scanner.scan(m_env);
 }
 
 expr parser::mk_sorry(pos_info const & p) {
@@ -302,7 +273,7 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
             m_env = ex.get_env();
             ex.get_exception().rethrow();
         }
-    } catch (show_goal_exception) {
+    } catch (break_at_pos_exception) {
         throw;
     } catch (parser_exception & ex) {
         CATCH(report_message(ex), throw);
@@ -1288,6 +1259,13 @@ static pair<notation::transition, parse_table> const * get_non_skip(list<pair<no
 expr parser::parse_notation(parse_table t, expr * left) {
     lean_assert(curr() == scanner::token_kind::Keyword);
     auto p = pos();
+    auto first_token = get_token_info().value();
+    auto check_break = [&]() {
+        if (check_break_at_pos(pos(), get_token_info().value())) {
+            // info is stored at position of first notation token
+            throw break_at_pos_exception(p, first_token);
+        }
+    };
     buffer<expr>                     args;
     buffer<notation::action_kind>    kinds;
     buffer<list<expr>>               nargs; // nary args
@@ -1309,6 +1287,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
         auto r = t.find(get_token_info().value());
         if (!r)
             break;
+        check_break();
         pair<notation::transition, parse_table> const * curr_pair = nullptr;
         if (tail(r)) {
             // There is more than one possible actions.
@@ -1345,12 +1324,14 @@ expr parser::parse_notation(parse_table t, expr * left) {
                 r_args.push_back(parse_expr(a.rbp()));
                 name sep = utf8_trim(a.get_sep().to_string()); // remove padding
                 while (curr_is_token(sep)) {
+                    check_break();
                     next();
                     r_args.push_back(parse_expr(a.rbp()));
                 }
             }
             if (terminator) {
                 if (curr_is_token(*terminator)) {
+                    check_break();
                     next();
                 } else {
                     throw parser_error(sstream() << "invalid composite expression, '" << *terminator << "' expected", pos());
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index b5a8cfec32..ded163fb23 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -77,12 +77,13 @@ struct snapshot {
 
 typedef std::vector<std::shared_ptr<snapshot const>> snapshot_vector;
 
-class show_goal_exception : public std::exception {
+class break_at_pos_exception : public std::exception {
 public:
-    pos_info m_pos;
-    tactic_state m_state;
+    pos_info    m_token_pos;
+    name        m_token;
 
-    show_goal_exception(pos_info const & pos, tactic_state const & goal) : m_pos(pos), m_state(goal) {}
+    break_at_pos_exception(pos_info const & token_pos, name const & token):
+            m_token_pos(token_pos), m_token(token) {}
 };
 
 enum class id_behavior {
@@ -139,6 +140,7 @@ class parser : public abstract_parser {
     // info support
     snapshot_vector *       m_snapshot_vector;
     name_set                m_old_buckets_from_snapshot;
+    optional<pos_info>      m_break_at_pos;
 
     // curr command token
     name                   m_cmd_token;
@@ -237,6 +239,8 @@ public:
            std::shared_ptr<snapshot const> const & s = {}, snapshot_vector * sv = nullptr);
     ~parser();
 
+    void set_break_at_pos(pos_info const & pos) { m_break_at_pos = some(pos); }
+    bool check_break_at_pos(pos_info const & p, name const & tk);
     void enable_show_goal(pos_info const & pos);
     void enable_show_info(pos_info const & pos);
 
diff --git a/src/shell/server.cpp b/src/shell/server.cpp
index 0a8809292a..b22efd6aa8 100644
--- a/src/shell/server.cpp
+++ b/src/shell/server.cpp
@@ -11,6 +11,7 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
 #include <vector>
 #include <clocale>
 #include "util/sexpr/option_declarations.h"
+#include "util/utf8.h"
 #include "library/mt_task_queue.h"
 #include "library/st_task_queue.h"
 #include "frontends/lean/parser.h"
@@ -245,7 +246,7 @@ void server::handle_request(server::cmd_req const & req) {
     } else if (command == "complete") {
         return handle_complete(req);
     } else if (command == "info") {
-        return send_msg(handle_info(req));
+        return handle_info(req);
     }
 
     send_msg(cmd_res(req.m_seq_num, std::string("unknown command")));
@@ -293,7 +294,7 @@ std::shared_ptr<snapshot const> get_closest_snapshot(std::shared_ptr<module_info
     auto snapshots = mod_info.get()->m_result.get().m_snapshots;
     auto ret = snapshots.size() ? snapshots.front() : std::shared_ptr<snapshot>();
     for (auto & snap : snapshots) {
-        if (snap->m_pos.first <= line)
+        if (snap->m_pos.first < line)
             ret = snap;
     }
     return ret;
@@ -352,29 +353,85 @@ void server::handle_complete(cmd_req const & req) {
     get_global_task_queue()->submit<auto_complete_task>(this, req.m_seq_num, pattern, mod_info, line);
 }
 
-server::cmd_res server::handle_info(server::cmd_req const & req) {
-    std::string fn = req.m_payload.at("file_name");
-    unsigned line = req.m_payload.at("line");
-    unsigned col = req.m_payload.at("column");
+class server::info_task : public task<unit> {
+    server * m_server;
+    unsigned m_seq_num;
+    std::shared_ptr<module_info const> m_mod_info;
 
-    auto opts = m_ios.get_options();
-    auto env = m_initial_env;
-    if (auto mod = m_mod_mgr->get_module(fn)->m_result.peek()) {
-        if (mod->m_loaded_module->m_env)
-            env = *mod->m_loaded_module->m_env;
-        if (!mod->m_snapshots.empty()) opts = mod->m_snapshots.back()->m_options;
+public:
+    info_task(server * server, unsigned seq_num, std::shared_ptr<module_info const> const & mod_info):
+            m_server(server), m_seq_num(seq_num), m_mod_info(mod_info) {}
+
+    // TODO(gabriel): find cleaner way to give it high prio
+    task_kind get_kind() const override { return task_kind::parse; }
+
+    virtual bool is_tiny() const override { return true; }
+
+    void description(std::ostream & out) const override {
+        out << "info at (" << get_pos().first << ", " << get_pos().second << ")";
     }
 
-    json record;
-    for (auto & infom : m_msg_buf->get_info_managers()) {
-        if (infom.get_file_name() == fn) {
-            infom.get_info_record(env, opts, m_ios, line, col, record);
+    std::vector<generic_task_result> get_dependencies() override {
+        return {m_mod_info->m_result};
+    }
+
+    // TODO(gabriel): handle cancellation
+
+    unit execute() override {
+        try {
+            pos_info pos = get_pos();
+            std::istringstream in(*m_mod_info->m_lean_contents);
+            json j;
+            if (auto snap = get_closest_snapshot(m_mod_info, pos.first)) {
+                snapshot s = *snap;
+                s.m_sub_buckets.clear(); // HACK
+                try {
+                    bool use_exceptions = true;
+                    parser p(s.m_env, get_global_ios(), mk_dummy_loader(), in, get_module_id(),
+                             use_exceptions, std::make_shared<snapshot>(s), nullptr);
+                    p.set_break_at_pos(pos);
+                    p();
+                } catch (break_at_pos_exception & e) {
+                    lean_assert(e.m_token_pos.first == pos.first);
+
+                    auto opts = m_server->m_ios.get_options();
+                    auto env = m_server->m_initial_env;
+                    if (auto mod = m_mod_info->m_result.peek()) {
+                        if (mod->m_loaded_module->m_env)
+                            env = *mod->m_loaded_module->m_env;
+                        if (!mod->m_snapshots.empty()) opts = mod->m_snapshots.back()->m_options;
+                    }
+
+                    json record;
+                    for (auto & infom : m_server->m_msg_buf->get_info_managers()) {
+                        if (infom.get_file_name() == get_module_id()) {
+                            infom.get_info_record(env, opts, m_server->m_ios, e.m_token_pos.first, e.m_token_pos.second,
+                                                  record);
+                        }
+                    }
+
+                    j["record"] = record;
+                }
+            }
+
+            m_server->send_msg(cmd_res(m_seq_num, j));
+        } catch (throwable & ex) {
+            m_server->send_msg(cmd_res(m_seq_num, std::string(ex.what())));
         }
+        return {};
     }
+};
 
-    json res;
-    res["record"] = record;
-    return { req.m_seq_num, res };
+void server::handle_info(server::cmd_req const & req) {
+    std::string fn = req.m_payload.at("file_name");
+    pos_info pos = {req.m_payload.at("line"), req.m_payload.at("column")};
+
+    scope_message_context scope_msg_ctx(message_bucket_id { "_server", 0 });
+    scoped_task_context scope_task_ctx(fn, pos);
+
+    auto mod_info = m_mod_mgr->get_module(fn);
+
+    get_global_task_queue()->submit<info_task>(this, req.m_seq_num, mod_info);
 }
 
 std::tuple<std::string, module_src, time_t> server::load_module(module_id const & id, bool can_use_olean) {
diff --git a/src/shell/server.h b/src/shell/server.h
index 80a31b3471..d038341ec0 100644
--- a/src/shell/server.h
+++ b/src/shell/server.h
@@ -55,7 +55,8 @@ class server : public module_vfs {
     cmd_res handle_sync(cmd_req const & req);
     class auto_complete_task;
     void handle_complete(cmd_req const & req);
-    cmd_res handle_info(cmd_req const & req);
+    class info_task;
+    void handle_info(cmd_req const & req);
 
 public:
     server(unsigned num_threads, environment const & intial_env, io_state const & ios);
diff --git a/src/util/utf8.cpp b/src/util/utf8.cpp
index 3110538b4b..23fe994988 100644
--- a/src/util/utf8.cpp
+++ b/src/util/utf8.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <cstdlib>
 #include <string>
 #include "util/debug.h"
+#include "util/optional.h"
 
 namespace lean {
 bool is_utf8_next(unsigned char c) { return (c & 0xC0) == 0x80; }
@@ -40,6 +41,19 @@ size_t utf8_strlen(char const * str) {
     return r;
 }
 
+optional<size_t> utf8_char_pos(char const * str, size_t char_idx) {
+    size_t r = 0;
+    while (*str != 0) {
+        if (char_idx == 0)
+            return some<size_t>(r);
+        char_idx--;
+        unsigned sz = get_utf8_size(*str);
+        r += sz;
+        str += sz;
+    }
+    return optional<size_t>();
+}
+
 char const * get_utf8_last_char(char const * str) {
     char const * r;
     lean_assert(*str != 0);
diff --git a/src/util/utf8.h b/src/util/utf8.h
index 455a149552..1f88315955 100644
--- a/src/util/utf8.h
+++ b/src/util/utf8.h
@@ -6,11 +6,13 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include "util/optional.h"
 
 namespace lean {
 bool is_utf8_next(unsigned char c);
 unsigned get_utf8_size(unsigned char c);
 size_t utf8_strlen(char const * str);
+optional<size_t> utf8_char_pos(char const * str, size_t char_idx);
 char const * get_utf8_last_char(char const * str);
 std::string utf8_trim(std::string const & s);
 }
diff --git a/tests/lean/interactive/info.input b/tests/lean/interactive/info.input
index 541320f12e..1e6dc1152e 100644
--- a/tests/lean/interactive/info.input
+++ b/tests/lean/interactive/info.input
@@ -1,2 +1,2 @@
 {"seq_num": 0, "command": "sync", "file_name": "f", "content": "definition f := tt"}
-{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 16}
+{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 17}
diff --git a/tests/lean/interactive/info_notation.input b/tests/lean/interactive/info_notation.input
new file mode 100644
index 0000000000..01db967777
--- /dev/null
+++ b/tests/lean/interactive/info_notation.input
@@ -0,0 +1,2 @@
+{"seq_num": 0, "command": "sync", "file_name": "f", "content": "def f := [tt]"}
+{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 12}
diff --git a/tests/lean/interactive/info_notation.input.expected.out b/tests/lean/interactive/info_notation.input.expected.out
new file mode 100644
index 0000000000..8ce34abc6e
--- /dev/null
+++ b/tests/lean/interactive/info_notation.input.expected.out
@@ -0,0 +1,2 @@
+{"message":"file invalidated","response":"ok","seq_num":0}
+{"record":{"full-id":"list.cons","source":{"column":10,"file":"/library/init/core.lean","line":189},"type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":1}
diff --git a/tests/lean/interactive/info_notation1.input b/tests/lean/interactive/info_notation1.input
new file mode 100644
index 0000000000..66b00e5d55
--- /dev/null
+++ b/tests/lean/interactive/info_notation1.input
@@ -0,0 +1,2 @@
+{"seq_num": 0, "command": "sync", "file_name": "f", "content": "def f := [tt]++[]"}
+{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 13}
diff --git a/tests/lean/interactive/info_notation1.input.expected.out b/tests/lean/interactive/info_notation1.input.expected.out
new file mode 100644
index 0000000000..520cf6a1bb
--- /dev/null
+++ b/tests/lean/interactive/info_notation1.input.expected.out
@@ -0,0 +1,2 @@
+{"message":"file invalidated","response":"ok","seq_num":0}
+{"record":{"full-id":"append","source":{"column":4,"file":"/library/init/core.lean","line":251},"type":"Π {α : Type} [_inst_1 : has_append α], α → α → α"},"response":"ok","seq_num":1}