location of current decl

Stream: metaprogramming / tactics

[Alex J. Best]

Is it possible from within TacticM to get the file location of the current declaration (or say the Syntax of the leading def theorem etc?).

[Alex J. Best]

I.e. imagine I wanted to write a tactic blah that prints the location of the example

...
stuff
...
example : False := by
  blah -- current declaration is at line 7 column 1

[Scott Morrison]

This isn't a complete answer, but maybe

def getSourceUpTo (s : Syntax) : CoreM (String × String) := do
  let fileMap := (← readThe Core.Context).fileMap
  let ({ line := line, column := _ }, _) := stxRange fileMap s
  ...

from branch#sagredo-widget is useful.