From cbedff5aba309861e1f02e0868849efc7658b868 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 21 Dec 2021 10:52:22 +0100 Subject: [PATCH] feat: optionally add information to all symbols during delaboration Add an option called pp.tagSymbols which, if set, makes the delaborator add term information to all symbols it can during delaboration. This option is disabled per default because it would break the LSP server's hovering behaviour. It is however useful when for example automatically generating interactive documentation. --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 10 ++++++++-- src/Lean/PrettyPrinter/Delaborator/Options.lean | 6 ++++++ 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 7d5fcda18b..1c7ae1c2a0 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -100,11 +100,17 @@ def delabConst : Delab := do c := `_root_ ++ c else c := c₀ - return mkIdent c + mkIdent c else `($(mkIdent c).{$[$(ls.toArray.map quote)],*}) - maybeAddBlockImplicit stx + let stx ← maybeAddBlockImplicit stx + if (←getPPOption getPPTagSymbols) then + let stx ← annotateCurPos stx + addTermInfo (←getPos) stx (←getExpr) + stx + else + stx structure ParamKind where name : Name diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 2188c59242..eaa495f3da 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -90,6 +90,11 @@ register_builtin_option pp.safeShadowing : Bool := { group := "pp" descr := "(pretty printer) allow variable shadowing if there is no collision" } +register_builtin_option pp.tagSymbols : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) tag symbol syntax with information" +} register_builtin_option pp.proofs : Bool := { defValue := false group := "pp" @@ -180,6 +185,7 @@ def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o) def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o) def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o) def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o) +def getPPTagSymbols (o : Options) : Bool := o.get pp.tagSymbols.name (getPPAll o) def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o) def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o) def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)