fix(frontends/lean/tactic_notation): report state after tactic execution on ,

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);

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;

tests/lean/interactive/info_goal.lean

@@ -2,6 +2,8 @@ example : ℕ → ℕ :=
 begin
   exact id
 --^ "command": "info"
+          ,
+        --^ "command": "info"
 end
 --^ "command": "info"
 

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}