From eb7bf2b272862940832ed63a5892a5c261fbe446 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 23 Apr 2022 17:42:32 +0200
Subject: [PATCH] fix: show single final state after tactic combinator

---
 src/Lean/Server/InfoUtils.lean                     | 12 ++++++++++--
 tests/lean/interactive/plainGoal.lean              |  1 +
 tests/lean/interactive/plainGoal.lean.expected.out |  6 ++++++
 3 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index fb9eda3c82..501a3842b7 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -221,9 +221,12 @@ structure GoalsAtResult where
   Moreover, we instruct the LSP server to use the state after tactic execution if
   - the hover position is after the info's start position *and*
   - there is no nested tactic info after the hover position (tactic combinators should decide for themselves
-    where to show intermediate states by calling `withTacticInfoContext`) -/
+    where to show intermediate states by calling `withTacticInfoContext`)
+
+  Finally, if the hover position is over the infos' trailing whitespace, we only show the last such info
+  (so that we only show the single final state after combinators such as `repeat`). -/
 partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := Id.run do
-  t.deepestNodes fun
+  let goals := t.deepestNodes fun
     | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
         let trailSize := i.stx.getTrailingSize
@@ -235,6 +238,11 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
       else
         failure
     | _, _, _ => none
+  if let (last :: _ :: _) := goals.reverse then
+    -- should be the same for any element in `goals`
+    if last.tacticInfo.stx.getTailPos?.get! <= hoverPos then
+      return [last]
+  goals
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool
     | InfoTree.node i@(Info.ofTacticInfo _) cs => Id.run do
diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean
index c23248f8d1..63d7362596 100644
--- a/tests/lean/interactive/plainGoal.lean
+++ b/tests/lean/interactive/plainGoal.lean
@@ -76,3 +76,4 @@ theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b := by
     rw [Nat.add_succ]
     repeat (rw [Nat.mul_succ])
                            --^ $/lean/plainGoal
+                            --^ $/lean/plainGoal
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 6d8764110d..57acb6fb2b 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -95,3 +95,9 @@
  ["t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * Nat.succ n✝",
   "t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)",
   "t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 76, "character": 30}}
+{"rendered":
+ "```lean\nt a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```",
+ "goals":
+ ["t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]}