feat: with_annotate_state helper tactic

src/Init/Notation.lean

@@ -219,6 +219,10 @@ macro_rules
 macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this []
 
 namespace Parser.Tactic
+declare_syntax_cat rawStx
+/-- `withAnnotateState stx t` annotates the lexical range of `stx : Syntax` with the initial and final state of running tactic `t`. -/
+scoped syntax (name := withAnnotateState) "with_annotate_state " rawStx ppSpace tactic : tactic
+
 /--
 Introduce one or more hypotheses, optionally naming and/or pattern-matching them.
 For each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -9,6 +9,12 @@ import Lean.Elab.Tactic.ElabTerm
 
 namespace Lean.Elab.Tactic
 open Meta
+open Parser.Tactic
+
+@[builtinTactic withAnnotateState] def evalWithAnnotateState : Tactic
+  | `(tactic| with_annotate_state $stx $t) =>
+    withTacticInfoContext stx (evalTactic t)
+  | _ => throwUnsupportedSyntax
 
 @[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ =>
   done