From e2bf4fcddb1840250938fa64439cb2ff6d241640 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Jan 2017 20:58:05 -0800
Subject: [PATCH] fix(frontends/lean/tactic_notation): add skip tactic to save
 intermediate result

@kha, this commit fixes the issue: comma before a `{}` block will show the state inside the block.
---
 src/frontends/lean/tactic_notation.cpp        |  4 ++
 tests/lean/interactive/goal_info.lean         | 40 +++++++++++++++++++
 .../interactive/goal_info.lean.expected.out   |  6 +++
 3 files changed, 50 insertions(+)
 create mode 100644 tests/lean/interactive/goal_info.lean
 create mode 100644 tests/lean/interactive/goal_info.lean.expected.out

diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 84c5674ab1..cb962e23c1 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -414,8 +414,12 @@ static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name c
                 /* parse next element */
                 expr next_tac;
                 if (p.curr_is_token(get_begin_tk())) {
+                    expr skip_tac = p.save_pos(mk_tactic_skip(p.env(), tac_class), pos);
+                    r = concat(p, r, skip_tac, start_pos, pos, tac_class);
                     next_tac = parse_begin_end_block(p, pos, get_end_tk(), tac_class);
                 } else if (p.curr_is_token(get_lcurly_tk())) {
+                    expr skip_tac = p.save_pos(mk_begin_end_element(mk_tactic_skip(p.env(), tac_class)), pos);
+                    r = concat(p, r, skip_tac, start_pos, pos, tac_class);
                     next_tac = parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class);
                 } else if (p.curr_is_token(get_do_tk())) {
                     expr tac = p.parse_expr();
diff --git a/tests/lean/interactive/goal_info.lean b/tests/lean/interactive/goal_info.lean
new file mode 100644
index 0000000000..96bbbbd758
--- /dev/null
+++ b/tests/lean/interactive/goal_info.lean
@@ -0,0 +1,40 @@
+constant addc {a b : nat} : a + b = b + a
+constant addassoc {a b c : nat} : (a + b) + c = a + (b + c)
+constant zadd (a : nat) : 0 + a = a
+
+open nat
+
+example : ∀ n m : ℕ, n + m = m + n :=
+begin
+  intros n m,
+  induction m with m' ih,
+                      --^ "command": "info"
+    { change n + 0 = 0 + n, simp [zadd] },
+--^ "command": "info"
+  { change succ (n + m') = succ m' + n,
+    rw [succ_add, ih]
+--^ "command":"info"
+  }
+end
+
+example : ∀ n m : ℕ, n + m = m + n :=
+begin
+  intros n m,
+  induction m with m' ih,
+  {   change n + 0 = 0 + n, simp [zadd] },
+   --^ "command": "info"
+  { change succ (n + m') = succ m' + n,
+    rw [succ_add, ih]
+  }
+end
+
+example : ∀ n m : ℕ, n + m = m + n :=
+begin
+  intros n m,
+  induction m with m' ih,
+  {   change n + 0 = 0 + n, simp [zadd] },
+                                     --^ "command": "info"
+  { change succ (n + m') = succ m' + n,
+    rw [succ_add, ih]
+  }
+end
diff --git a/tests/lean/interactive/goal_info.lean.expected.out b/tests/lean/interactive/goal_info.lean.expected.out
new file mode 100644
index 0000000000..33d6c9a09a
--- /dev/null
+++ b/tests/lean/interactive/goal_info.lean.expected.out
@@ -0,0 +1,6 @@
+{"message":"file invalidated","response":"ok","seq_num":0}
+{"record":{"state":"n : ℕ\n⊢ n + 0 = 0 + n\n\nn m' : ℕ,\nih : n + m' = m' + n\n⊢ n + succ m' = succ m' + n"},"response":"ok","seq_num":11}
+{"record":{"state":"n : ℕ\n⊢ n + 0 = 0 + n\n\nn m' : ℕ,\nih : n + m' = m' + n\n⊢ n + succ m' = succ m' + n"},"response":"ok","seq_num":13}
+{"record":{"state":"n m' : ℕ,\nih : n + m' = m' + n\n⊢ succ (n + m') = succ m' + n"},"response":"ok","seq_num":16}
+{"record":{"state":"n : ℕ\n⊢ n + 0 = 0 + n"},"response":"ok","seq_num":25}
+{"record":{"state":"no goals"},"response":"ok","seq_num":36}