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. -/