fix: partial fix of focus goal state

src/Lean/Elab/Tactic/Basic.lean

@@ -356,8 +356,13 @@ private def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do
 @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx =>
   withRef stx[2] <| focusAndDone <| evalManyTacticOptSemi stx[1]
 
-@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx =>
-  focus <| evalTactic stx[1]
+@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do
+  let mctxBefore  ← getMCtx
+  let goalsBefore ← getGoals
+  focus do
+    -- show focused state on `focus`
+    withInfoContext (pure ()) (mkTacticInfo mctxBefore goalsBefore stx[0])
+    evalTactic stx[1]
 
 private def getOptRotation (stx : Syntax) : Nat :=
   if stx.isNone then 1 else stx[0].toNat

tests/lean/interactive/plainGoal.lean

@@ -27,3 +27,10 @@ example (h1 : n = m) (h2 : m = 0) : 0 = n := by
  --^ $/lean/plainGoal
        --^ $/lean/plainGoal
            --^ $/lean/plainGoal
+
+example : 0 + n = n := by
+  induction n
+  focus
+ --^ $/lean/plainGoal
+    rfl
+-- TODO: goal state after dedent

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

@@ -48,3 +48,7 @@
  "position": {"line": 25, "character": 13}}
 {"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = 0\n```",
  "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = 0"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 32, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",
+ "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]}