From 35179809a2cfce3ee9196a41251aa3ca9d62d45d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jan 2020 15:33:02 -0800
Subject: [PATCH] feat: hide macro scopes encoding when displaying errors

---
 src/Init/Lean/Elab/Term.lean | 7 +++----
 src/Init/Lean/Elab/Util.lean | 8 ++++++++
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 73ecacf2a8..22785e628d 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -769,10 +769,9 @@ match result? with
 | none =>
   let process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do {
     when candidates.isEmpty $ do {
-      -- TODO: improve pretty printing
-      -- let extractionResult := extractMacroScopes n;
-      -- env ← getEnv;
-      throwError ref ("unknown identifier '" ++ toString n ++ "'")
+      mainModule ← getMainModule;
+      let view := extractMacroScopes n;
+      throwError ref ("unknown identifier '" ++ view.format mainModule ++ "'")
     };
     mkConsts ref candidates explicitLevels
   };
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index 2c47d4af3f..e068d4f139 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -14,6 +14,14 @@ match stx.truncateTrailing.reprint with -- TODO use syntax pretty printer
 | some str => format str.toFormat
 | none     => format stx
 
+def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format :=
+format $
+  if view.scopes.isEmpty then view.name
+  else if view.mainModule == mainModule then
+   view.scopes.foldl mkNameNum (view.name ++ view.imported)
+  else
+   view.scopes.foldl mkNameNum (view.name ++ view.imported ++ view.mainModule)
+
 namespace Elab
 
 structure MacroStackElem :=