feat: abbreviate names based on the namespace of the declaration (#260)

leanprover · Jan 20, 2025 · e9d995e · e9d995e
1 parent 8c60540
commit e9d995e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean
@@ -50,7 +50,8 @@ def Info.ofTypedName (n : Name) (t : Expr) : MetaM Info := do
   -- Use the main signature delaborator. We need to run sanitization, parenthesization, and formatting ourselves
   -- to be able to extract the pieces of the signature right before they are formatted
   -- and then format them individually.
-  let (sigStx, infos) ← PrettyPrinter.delabCore t (delab := PrettyPrinter.Delaborator.delabConstWithSignature.delabParams {} default #[])
+  let (sigStx, infos) ← withTheReader Core.Context ({ · with currNamespace := n.getPrefix }) <|
+    PrettyPrinter.delabCore t (delab := PrettyPrinter.Delaborator.delabConstWithSignature.delabParams {} default #[])
   let sigStx := (sanitizeSyntax sigStx).run' { options := (← getOptions) }
   let sigStx ← PrettyPrinter.parenthesize PrettyPrinter.Delaborator.declSigWithId.parenthesizer sigStx
   let `(PrettyPrinter.Delaborator.declSigWithId| $_:term $binders* : $type) := sigStx