From cea1fa303685cf7e5ff68e4ce3f643680a288418 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 11 Aug 2019 15:59:10 -0700 Subject: [PATCH] feat(library/init/lean/elaborator/command): display position information at `#resolve_name` --- library/init/lean/elaborator/basic.lean | 5 +++++ library/init/lean/elaborator/command.lean | 3 ++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean index 532fcb0b05..773215849a 100644 --- a/library/init/lean/elaborator/basic.lean +++ b/library/init/lean/elaborator/basic.lean @@ -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; diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean index b9695f23c8..56d0091877 100644 --- a/library/init/lean/elaborator/command.lean +++ b/library/init/lean/elaborator/command.lean @@ -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. -/