From db2a9121125b0cd3e7dce41b74c08dbea9b41c66 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 25 Apr 2022 14:00:14 +0200
Subject: [PATCH] feat: `with_annotate_state` helper tactic

---
 src/Init/Notation.lean                  | 4 ++++
 src/Lean/Elab/Tactic/BuiltinTactic.lean | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 432dea5231..243e1d959c 100644
--- a/src/Init/Notation.lean
+++ b/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.
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index f84cfce785..fdbf41a5e9 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/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