feat: show initial state for tactic combinators by default

src/Lean/Elab/SyntheticMVars.lean

@@ -8,7 +8,7 @@ import Lean.Elab.Term
 import Lean.Elab.Tactic.Basic
 
 namespace Lean.Elab.Term
-open Tactic (TacticM evalTactic getUnsolvedGoals mkTacticInfo)
+open Tactic (TacticM evalTactic getUnsolvedGoals withTacticInfoContext)
 open Meta
 
 /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
@@ -211,13 +211,7 @@ mutual
     modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
     let remainingGoals ← withInfoHole mvarId <|
       liftTacticElabM mvarId do
-        let mctxBefore  ← getMCtx
-        -- NOTE: we need an outer node as `withInfoHole` discards all trees but the last one
-        withInfoContext (do
-            -- push separate leaf for `by` so we show the initial state on the whole token
-            pushInfoLeaf (← mkTacticInfo mctxBefore [mvarId] byTk)
-            evalTactic code)
-          (mkTacticInfo mctxBefore [mvarId] tacticCode)
+        withTacticInfoContext tacticCode (evalTactic code)
         getUnsolvedGoals
     unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals
 

src/Lean/Elab/Tactic/Basic.lean

@@ -95,6 +95,20 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 
+def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info :=
+  return Info.ofTacticInfo {
+    mctxBefore    := mctxBefore
+    goalsBefore   := goalsBefore
+    stx           := stx
+    mctxAfter     := (← getMCtx)
+    goalsAfter    := (← getGoals)
+  }
+
+@[inline] def withTacticInfoContext (stx : Syntax) (x : TacticM α) : TacticM α := do
+  let mctxBefore  ← getMCtx
+  let goalsBefore ← getGoals
+  withInfoContext x (mkTacticInfo mctxBefore goalsBefore stx)
+
 mutual
 
   partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit :=
@@ -132,19 +146,8 @@ mutual
           | none         => expandTacticMacro stx
       | _ => throwError "unexpected command"
 
-  partial def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info :=
-    return Info.ofTacticInfo {
-      mctxBefore    := mctxBefore
-      goalsBefore   := goalsBefore
-      stx           := stx
-      mctxAfter     := (← getMCtx)
-      goalsAfter    := (← getGoals)
-    }
-
-  partial def evalTactic (stx : Syntax) : TacticM Unit := do
-    let mctxBefore  ← getMCtx
-    let goalsBefore ← getGoals
-    withInfoContext (evalTacticAux stx) (mkTacticInfo mctxBefore goalsBefore stx)
+  partial def evalTactic (stx : Syntax) : TacticM Unit :=
+    withTacticInfoContext stx (evalTacticAux stx)
 
 end
 
@@ -155,9 +158,7 @@ end
 -/
 def saveTacticInfoForToken (stx : Syntax) : TacticM Unit := do
   unless stx.getPos?.isNone do
-    let mctxBefore  ← getMCtx
-    let goalsBefore ← getGoals
-    withInfoContext (pure ()) (mkTacticInfo mctxBefore goalsBefore stx)
+    withTacticInfoContext stx (pure ())
 
 /- Elaborate `x` with `stx` on the macro stack -/
 @[inline]

src/Lean/Server/FileWorker.lean

@@ -609,10 +609,10 @@ section RequestHandling
       if let (some pos, some tailPos) := (stx.getPos?, stx.getTailPos?) then
         for t in (← read).infoState.trees do
           for ti in t.deepestNodes (fun
-            | _, i@(Elab.Info.ofTermInfo ti) => match i.pos? with
+            | _, i@(Elab.Info.ofTermInfo ti), _ => match i.pos? with
               | some ipos => if pos <= ipos && ipos < tailPos then some ti else none
               | _         => none
-            | _, _ => none) do
+            | _, _, _ => none) do
             match ti.expr with
             | Expr.fvar .. => addToken ti.stx SemanticTokenType.variable
             | _            => if ti.stx.getPos?.get! > pos then addToken ti.stx SemanticTokenType.property

src/Lean/Server/InfoUtils.lean

@@ -13,17 +13,16 @@ namespace Lean.Elab
 /--
   For every branch, find the deepest node in that branch matching `p`
   with a surrounding context (the innermost one) and return all of them. -/
-partial def InfoTree.deepestNodes (p : ContextInfo → Info → Option α) : InfoTree → List α :=
+partial def InfoTree.deepestNodes (p : ContextInfo → Info → Std.PersistentArray InfoTree → Option α) : InfoTree → List α :=
   go none
 where go ctx?
   | context ctx t => go ctx t
   | n@(node i cs) =>
-    let cs := cs.toList
-    let ccs := cs.map (go <| i.updateContext? ctx?)
-    let cs := ccs.join
-    if !cs.isEmpty then cs
+    let ccs := cs.toList.map (go <| i.updateContext? ctx?)
+    let cs' := ccs.join
+    if !cs'.isEmpty then cs'
     else match ctx? with
-      | some ctx => match p ctx i with
+      | some ctx => match p ctx i cs with
         | some a => [a]
         | _      => []
       | _        => []
@@ -86,7 +85,7 @@ def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option Nat := Option
   return hoverPos - tailPos
 
 def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) :=
-  let ts := t.deepestNodes fun ctx i => if p i then some (ctx, i) else none
+  let ts := t.deepestNodes fun ctx i _ => if p i then some (ctx, i) else none
 
   let infos := ts.map fun (ci, i) =>
     let diff := i.tailPos?.get! - i.pos?.get!
@@ -160,18 +159,34 @@ structure GoalsAtResult where
   - None of the `children` can provide 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 >= endPos
+  Moreover, we instruct the LSP server to use the state after the tactic execution if hoverPos >= endPos *and*
+  there is no nested tactic info (i.e. it is a leaf tactic; tactic combinators should decide for themselves
+  where to show intermediate/final states)
 -/
 partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := do
   t.deepestNodes fun
-    | ctx, i@(Info.ofTacticInfo ti) => OptionM.run do
+    | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do
       let (some pos, some tailPos) ← pure (i.pos?, i.tailPos?)
         | failure
       let trailSize := i.stx.getTrailingSize
       -- NOTE: include position just after tactic, i.e. when the cursor is still adjacent
       -- (even when `trailSize == 0`, which is the case at EOF)
       guard <| pos ≤ hoverPos ∧ hoverPos < tailPos + Nat.max 1 trailSize
-      return { ctxInfo := ctx, tacticInfo := ti, useAfter := hoverPos > pos }
-    | _, _ => none
+      return { ctxInfo := ctx, tacticInfo := ti, useAfter :=
+        hoverPos > pos && !cs.any (hasNestedTactic pos tailPos) }
+    | _, _, _ => none
+where
+  hasNestedTactic (pos tailPos) : InfoTree → Bool
+    | InfoTree.node (Info.ofTacticInfo ti) cs => do
+      if let `(by $t) := ti.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
+        -- ignore nested infos of the same tactic, e.g. from expansion
+        if (pos', tailPos') != (pos, tailPos) then
+          return true
+      cs.any (hasNestedTactic pos tailPos)
+    | InfoTree.node (Info.ofMacroExpansionInfo _) cs =>
+      cs.any (hasNestedTactic pos tailPos)
+    | _ => false
 
 end Lean.Elab

tests/lean/infoTree.lean.expected.out

@@ -81,7 +81,7 @@
     y : Nat @ ⟨18, 8⟩-⟨18, 9⟩
     Bool : Type @ ⟨18, 10⟩-⟨18, 11⟩
     b : Bool @ ⟨18, 10⟩-⟨18, 11⟩
-    Tactic @ ⟨19, 4⟩-⟨19, 8⟩
+    Tactic @ ⟨18, 15⟩-⟨19, 8⟩
     before 
     x y : Nat
     b : Bool
@@ -99,6 +99,12 @@
         b : Bool
         ⊢ x + 0 = x
         after no goals
+          Tactic @ ⟨19, 4⟩-⟨19, 8⟩
+          before 
+          x y : Nat
+          b : Bool
+          ⊢ x + 0 = x
+          after no goals
 [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩
   Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩
     Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩

tests/lean/interactive/plainGoal.lean

@@ -4,7 +4,9 @@ example : α → α := by
   intro a
 --^ $/lean/plainGoal
  --^ $/lean/plainGoal
-  apply a
+ --v $/lean/plainGoal
+  focus
+    apply a
 
 example : α → α := by
                   --^ $/lean/plainGoal

tests/lean/interactive/plainGoal.lean.expected.out

@@ -15,6 +15,10 @@
 {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
  "goals": ["α : Sort ?u\na : α\n⊢ α"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 8, "character": 20}}
+ "position": {"line": 7, "character": 3}}
+{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
+ "goals": ["α : Sort ?u\na : α\n⊢ α"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 10, "character": 20}}
 {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
  "goals": ["α : Sort ?u\n⊢ α → α"]}