max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/elaborator/command): display position information at #resolve_name

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-11 15:59:10 -07:00
parent 4fe9c30d6f
commit cea1fa3036
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/elaborator/basic.lean
View file

@ -214,6 +214,11 @@ mkElabAttribute `commandTerm "command" builtinCommandElabTable
@[init mkCommandElabAttribute]
constant commandElabAttribute : CommandElabAttribute := default _
def getPosition (pos : Option String.Pos := none) : Elab Position :=
do ctx ← read;
s ← get;
pure $ ctx.fileMap.toPosition (pos.getOrElse s.cmdPos)
def mkMessage (msg : String) (pos : Option String.Pos := none) : Elab Message :=
do ctx ← read;
s ← get;

3
library/init/lean/elaborator/command.lean
View file

@ -191,7 +191,8 @@ fun _ => do
fun n => do
let id := n.getIdAt 1;
resolvedIds ← resolveName id;
runIO (IO.println resolvedIds);
pos ← getPosition;
runIO (IO.println (toString pos ++ " " ++ toString resolvedIds));
pure ()
/- We just ignore Lean3 notation declaration commands. -/