From 8ae726203dfe4286d14dd186ad752dccc455e24a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 12 May 2021 10:51:42 +0200
Subject: [PATCH] fix: plainGoal: consider original positions only when
 deciding whether a tactic is a combinator

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

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index ffc97d88d5..a1aaa050a8 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -156,7 +156,7 @@ structure GoalsAtResult where
   Try to retrieve `TacticInfo` for `hoverPos`.
   We retrieve the `TacticInfo` `info`, if there is a node of the form `node (ofTacticInfo info) children` s.t.
   - `hoverPos` is sufficiently inside `info`'s range (see code), and
-  - None of the `children` can provide satisfy the condition above. That is, for composite tactics such as
+  - None of the `children` satisfy the condition above. That is, for composite tactics such as
     `induction`, we always give preference for information stored in nested (children) tactics.
 
   Moreover, we instruct the LSP server to use the state after the tactic execution if `hoverPos > pos` *and*
@@ -184,10 +184,10 @@ partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List Goal
   return rs
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool
-    | InfoTree.node (Info.ofTacticInfo ti) cs => do
-      if let `(by $t) := ti.stx then
+    | InfoTree.node i@(Info.ofTacticInfo _) cs => do
+      if let `(by $t) := i.stx then
         return false  -- ignore term-nested proofs such as in `simp [show p by ...]`
-      if let (some pos', some tailPos') := (ti.stx.getPos?, ti.stx.getTailPos?) then
+      if let (some pos', some tailPos') := (i.pos?, i.tailPos?) then
         -- ignore nested infos of the same tactic, e.g. from expansion
         if (pos', tailPos') != (pos, tailPos) then
           return true
diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean
index 894a63cc72..3e9791603c 100644
--- a/tests/lean/interactive/plainGoal.lean
+++ b/tests/lean/interactive/plainGoal.lean
@@ -42,3 +42,7 @@ example : 0 + n = n := by
 example : 0 + n = n := by
   cases n with
  --^ $/lean/plainGoal
+
+example : ∀ a b : Nat, a = b := by
+  intro a b
+ --^ $/lean/plainGoal
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 4a61a4cd6a..7a313cc870 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -59,3 +59,7 @@
  "position": {"line": 42, "character": 3}}
 {"rendered": "```lean\nn : Nat\n⊢ 0 + n = n\n```",
  "goals": ["n : Nat\n⊢ 0 + n = n"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 46, "character": 3}}
+{"rendered": "```lean\na b : Nat\n⊢ a = b\n```",
+ "goals": ["a b : Nat\n⊢ a = b"]}