tactic for entire declaration up to tactic invocation

Stream: general

[Frederick Pu]

I want to make a tactic womp such that the entire theorem declaration and proof up to the invocation of the tactic is printed. Namely start where the theorem keyword starts and end at the column and line number where womp starts.
For example in the following code block:

theorem lol : (a * b) * c = c * a * b := by
     cases em (2 + 2 = 0) with
     | inl => womp
     | inr => by ring

womp would output:

theorem lol : (a * b) * c = c * a * b := by
     cases em (2 + 2 = 0) with
     | inl =>

I'm thinking about doing something along these lines

import Lean.Elab.Tactic
import Lean.Syntax

open Lean.Elab.Tactic
open Lean.Syntax

def womp : TacticM Unit := do
  let stx ← getRef
  let pos ← getPosition stx
  let fileMap ← getFileMap
  let decl ← getDeclFor stx
  match decl with
  | some decl =>
    let declPos := fileMap.getPosition decl.range.start
    let targetPos := fileMap.getPosition pos.start
    let declString := fileMap.source.extract declPos targetPos
    logInfo declString
  | none =>
    logInfo "Could not find declaration."

But I don't what the correct api calls are to make this pseudo code actually work

[Frederick Pu]

nvm LLMLean already does this