feat: show state on by

src/Lean/Elab/InfoTree.lean

@@ -268,10 +268,6 @@ def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
       pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := stx }
   return ns
 
-def mkInfoNode (info : Info) : m Unit := do
-  if (← getInfoState).enabled then
-    modifyInfoTrees fun ts => PersistentArray.empty.push <| InfoTree.node info ts
-
 @[inline] def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees

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)
+open Tactic (TacticM evalTactic getUnsolvedGoals mkTacticInfo)
 open Meta
 
 /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
@@ -205,11 +205,20 @@ mutual
         modify fun s => { s with syntheticMVars := savedSyntheticMVars }
 
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
-    /- Recall, `tacticCode` is the whole `by ...` expression.
-       We store the `by` because in the future we want to save the initial state information at the `by` position. -/
+    /- Recall, `tacticCode` is the whole `by ...` expression. -/
+    let byTk := tacticCode[0]
     let code := tacticCode[1]
     modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
-    let remainingGoals ← withInfoHole mvarId do liftTacticElabM mvarId do evalTactic code; getUnsolvedGoals
+    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)
+        getUnsolvedGoals
     unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals
 
   /-- Try to synthesize the given pending synthetic metavariable. -/

tests/lean/interactive/plainGoal.lean

@@ -1,5 +1,10 @@
 example : α → α := by
+                  --^ $/lean/plainGoal
+                   --^ $/lean/plainGoal
   intro a
 --^ $/lean/plainGoal
  --^ $/lean/plainGoal
   apply a
+
+example : α → α := by
+                  --^ $/lean/plainGoal

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

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