diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index cbfa40ddc0..666621f156 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -254,6 +254,7 @@ public:
 
     void set_break_at_pos(pos_info const & pos) { m_break_at_pos = some(pos); }
     optional<pos_info> const & get_break_at_pos() const { return m_break_at_pos; }
+    bool get_complete() { return m_complete; }
     void set_complete(bool complete) { m_complete = complete; }
     /** \brief Throw \c break_at_pos_exception with given context if \c m_break_at_pos is inside current token. */
     void check_break_at_pos(break_at_pos_exception::token_context ctxt = break_at_pos_exception::token_context::none);
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 9cab95e5f7..84c5674ab1 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -426,6 +426,9 @@ static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name c
                 }
                 r = concat(p, r, next_tac, start_pos, pos, tac_class);
                 if (!p.curr_is_token(end_token)) {
+                    // small 'info' tweak: on `,`, report tactic state at following token instead
+                    if (!p.get_complete() && p.get_break_at_pos() == some(p.pos()))
+                        p.set_break_at_pos({p.pos().first, p.pos().second + 1});
                     p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
                 }
             } catch (break_at_pos_exception & ex) {
@@ -439,7 +442,12 @@ static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name c
         throw;
     }
     auto end_pos = p.pos();
-    p.next();
+    try {
+        p.next();
+    } catch (break_at_pos_exception & ex) {
+        ex.report_goal_pos(end_pos);
+        throw;
+    }
     r = p.save_pos(mk_begin_end_block(r), end_pos);
     if (!is_ext_tactic_class) {
         return r;
diff --git a/tests/lean/interactive/info_goal.lean b/tests/lean/interactive/info_goal.lean
index 99815353cd..49caf9f332 100644
--- a/tests/lean/interactive/info_goal.lean
+++ b/tests/lean/interactive/info_goal.lean
@@ -2,6 +2,8 @@ example : ℕ → ℕ :=
 begin
   exact id
 --^ "command": "info"
+          ,
+        --^ "command": "info"
 end
 --^ "command": "info"
 
diff --git a/tests/lean/interactive/info_goal.lean.expected.out b/tests/lean/interactive/info_goal.lean.expected.out
index dc9541e92f..df7026d464 100644
--- a/tests/lean/interactive/info_goal.lean.expected.out
+++ b/tests/lean/interactive/info_goal.lean.expected.out
@@ -1,4 +1,5 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":126},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4}
 {"record":{"state":"no goals"},"response":"ok","seq_num":6}
-{"record":{"state":"⊢ ℕ → ℕ"},"response":"ok","seq_num":9}
+{"record":{"state":"no goals"},"response":"ok","seq_num":8}
+{"record":{"state":"⊢ ℕ → ℕ"},"response":"ok","seq_num":11}